bench(bz): certifying series for kernel_factor_sweep.py, measuring irreducible_cert against the kernel-factor curve (Deliverable 4 of #8566)

[kim-em]

Goal: Deliverable 4 of #8566: quantify the certificate architecture's payoff by adding a certifying series to the kernel-factor sweep. Split out of #8566 because the sweep harness lives only on the unmerged kernel-decide-series branch, exactly as that issue's dependency note anticipated ("land or rebase that branch first, or scope this deliverable as a follow-up commit on it").

Current state.

• The irreducible_cert tactic is in (feat(bz): irreducible_cert tactic — kernel-checked certifying irreducibility (Part 2 of #8552) #8566): for Irreducible (HexPolyZMathlib.toPolynomial f) goals it runs Hex.certifyIrreducible? compiled at elaboration time, reifies the certificate (HexBerlekampZassenhausMathlib/CertReify.lean), and the kernel replays only Hex.checkIrreducibleCertLinear (incremental pow-chain comparison, O(n · p) per modular factor) plus the primality / content / degree side checks on literal data. End-to-end examples: HexBerlekampZassenhausMathlib/IrreducibleCertTest.lean.
• scripts/bench/kernel_factor_sweep.py and reports/hexbz-kernel-factor.md exist only on kernel-decide-series (2 commits ahead of main: the timing harness + the frontier record for the "kernel runs factor under decide" curve).

Deliverables.

1. Land or rebase the kernel-decide-series branch (its own PR; it is a self-contained bench harness).
2. Extend scripts/bench/kernel_factor_sweep.py with a certifying series: per degree, time the by irreducible_cert proof against the existing kernel-factor curve, on irreducible families the generator covers: inert-prime-friendly families, NOT Swinnerton-Dyer (the per-prime degree-sum obstruction cannot certify balanced factorizations; certifyIrreducible? correctly returns none there). Exclude compiled prep from the headline number if the harness can split elaboration time; otherwise report both.
3. Record the Linear-vs-Incremental empirical comparison the feat(bz): irreducible_cert tactic — kernel-checked certifying irreducibility (Part 2 of #8552) #8566 checker deferred: checkIrreducibleCertLinear currently replays via checkIrreducibilityCertificateLinearIncremental on the analytic O(n · p) vs O(Σ p^k) argument; confirm (or refute) on the sweep families and note the result in reports/hexbz-kernel-factor.md.
4. Keep the sweep a not-in-CI diagnostic, per the feat(bz): certifying irreducibility — compiled certificate prep + kernel-checked verification #8552 scope note and SPEC/benchmarking.md.

Context. Note the tactic cannot run under bare lake env lean on a scratch file (the Hex.ZMod64.mul extern needs the precompiled dylibs that only lake-built modules load); the sweep should drive it through lake builds of generated modules, mirroring how the existing kernel-factor series works.

Verification. Sweep runs green locally on at least one inert-prime family; reports/hexbz-kernel-factor.md gains the certifying curve and the Linear-vs-Incremental note; no CI wiring.

🤖 Prepared with Claude Code