bench: Swinnerton-Dyer tier-crossover ladders with scaling figures

bench/HexBerlekampZassenhaus/Bench.lean

@@ -108,6 +108,12 @@ Gating external comparator:
   verified-Isabelle pairs for the HO-2 adversarial singletons (one new
   registration per distinct singleton input not already covered by
   `runIsabelleFactorChecksum`).
+* `runFactorAdvSwinnertonDyer{Ladder,Pair,SD4Blocks}Checksum`: the
+  Swinnerton-Dyer tier-crossover ladders (`SD_k`, `SD_k(x)·SD_k(x+1)`,
+  `∏_{i<m} SD_4(x+i)`), the tracked form of #8537's benchmark data, with
+  `runIsabelleAdvSwinnertonDyer{SD4,SD5,PairK2,PairK3,PairK4,SD4BlocksM3,
+  SD4BlocksM4}Checksum` verified-Isabelle rungs. All `scheduled-hardware`;
+  figures at `reports/figures/hex-berlekamp-zassenhaus-sd-*.svg`.
 * `runIsabelleFallbackProbeN{11,12,13,15,18,22,24}Checksum`: per-rung
   verified-Isabelle pairs for the cascade-trigger fallback-probe schedule. The
   `expectedHash` field is `none` on these registrations to keep elaboration off
@@ -127,6 +133,9 @@ namespace BerlekampZassenhausBench
 
 open Lean (Json)
 
+/-- Default for the ladder preps' loud out-of-range panics (`#[…][i]!`). -/
+local instance : Inhabited ZPoly := ⟨0⟩
+
 private instance benchBoundsThirtyOne : ZMod64.Bounds 31 := ⟨by decide, by decide⟩
 
 instance : Hashable ZPoly where
@@ -185,6 +194,77 @@ def advSwinnertonDyerSD3 : ZPoly :=
 def advPhi15 : ZPoly :=
   DensePoly.ofCoeffs #[1, -1, 0, 1, -1, 1, 0, -1, 1]
 
+/-- Swinnerton-Dyer `SD_4` (minimal polynomial of `√2+√3+√5+√7`, degree 16). -/
+def advSwinnertonDyerSD4 : ZPoly :=
+  DensePoly.ofCoeffs #[46225, 0, -5596840, 0, 13950764, 0, -7453176, 0, 1513334, 0,
+    -141912, 0, 6476, 0, -136, 0, 1]
+
+/-- Swinnerton-Dyer `SD_5` (minimal polynomial of `√2+√3+√5+√7+√11`, degree 32). -/
+def advSwinnertonDyerSD5 : ZPoly :=
+  DensePoly.ofCoeffs #[2000989041197056, 0, -44660812492570624, 0, 183876928237731840, 0,
+    -255690851718529024, 0, 172580952324702208, 0, -65892492886671360, 0,
+    15459151516270592, 0, -2349014746136576, 0, 239210760462336, 0, -16665641517056, 0,
+    801918722048, 0, -26625650688, 0, 602397952, 0, -9028096, 0, 84864, 0, -448, 0, 1]
+
+/--
+The Swinnerton-Dyer ladder `SD_1 … SD_5`: `SD_k` is the minimal polynomial of
+`√2 + … + √p_k` (degree `2^k`), irreducible over `ℤ` but splitting into
+degree-≤ 2 local factors mod every prime, so the classical tier must enumerate
+its whole head-forced subset powerset (`2^(r-1)` candidates at `r = 2^(k-1)`)
+to certify irreducibility. Coefficients pinned from sympy
+`minimal_polynomial`; the `SD_3` entry is the existing HO-2 fixture.
+-/
+def advSwinnertonDyerLadder : Array ZPoly := #[
+  DensePoly.ofCoeffs #[-2, 0, 1],
+  DensePoly.ofCoeffs #[1, 0, -10, 0, 1],
+  advSwinnertonDyerSD3,
+  advSwinnertonDyerSD4,
+  advSwinnertonDyerSD5]
+
+#guard advSwinnertonDyerLadder.map (·.degree?.getD 0) = #[2, 4, 8, 16, 32]
+
+/-- `p(x + a)`: Taylor shift via composition with `x + a`. -/
+def shiftArg (p : ZPoly) (a : Int) : ZPoly :=
+  DensePoly.compose p (DensePoly.ofCoeffs #[a, 1])
+
+#guard shiftArg (DensePoly.ofCoeffs #[-2, 0, 1]) 1 = DensePoly.ofCoeffs #[-1, 2, 1]
+
+/--
+The tier-crossover pair ladder `SD_k(x) · SD_k(x+1)` (degree `2^(k+1)`, two
+`2^(k-1)`-blocks of local factors). The classical tier answers `k ≤ 4` within
+its subset budget; at `k = 5` reaching the 16-blocks needs `ΣC(31,≤15) ≈ 2^30`
+candidates, so classical declines at its level boundary and the CLD lattice
+tier answers. This is the family behind #8530/#8537.
+-/
+def advSwinnertonDyerPair (k : Nat) : ZPoly :=
+  let p := advSwinnertonDyerLadder[k - 1]!
+  p * shiftArg p 1
+
+-- Constant coefficients of the derived products, pinned against the sympy
+-- reference expansion (2026-07-02) so a `compose`/`mul` regression cannot
+-- silently change the benchmark inputs.
+#guard (advSwinnertonDyerPair 1).coeff 0 = 2
+#guard (advSwinnertonDyerPair 2).coeff 0 = -8
+#guard (advSwinnertonDyerPair 3).coeff 0 = -40896
+#guard (advSwinnertonDyerPair 4).coeff 0 = 107460921600
+#guard (advSwinnertonDyerPair 5).coeff 0 = 11101827931906700692775396966400
+#guard (advSwinnertonDyerPair 5).degree?.getD 0 = 64
+
+/--
+The block-count ladder `∏_{i<m} SD_4(x+i)` (degree `16·m`, `m` blocks of eight
+quadratic local factors mod the chosen prime). The classical tier answers
+`m ≤ 2`; from `m = 3` the winning subsets sit past the classical tier's
+level-aware budget boundary (#8537), so it declines and the CLD lattice tier
+answers. The `m = 3` rung is the crossover measured in #8537's benchmark data.
+-/
+def advSwinnertonDyerSD4Blocks (m : Nat) : ZPoly :=
+  (List.range m).foldl (fun acc i => acc * shiftArg advSwinnertonDyerSD4 (Int.ofNat i)) 1
+
+#guard (advSwinnertonDyerSD4Blocks 2).coeff 0 = 107460921600
+#guard (advSwinnertonDyerSD4Blocks 3).coeff 0 = -1039528705604601600
+#guard (advSwinnertonDyerSD4Blocks 4).coeff 0 = -30893529063662744356454400
+#guard (advSwinnertonDyerSD4Blocks 4).degree?.getD 0 = 64
+
 /-- Prepared split input whose single parameter encodes degree and height. -/
 structure DegreeHeightInput where
   degree : Nat
@@ -481,6 +561,41 @@ def prepAdvSwinnertonDyerSD3 (_ : Nat) : ZPoly :=
 def prepAdvPhi15 (_ : Nat) : ZPoly :=
   advPhi15
 
+/-- Prep for the Swinnerton-Dyer ladder: parameter `k` selects `SD_k`.
+Panics (rather than silently substituting a rung) outside the registered
+`k = 1..5` schedule. -/
+def prepAdvSwinnertonDyerLadder (k : Nat) : ZPoly :=
+  advSwinnertonDyerLadder[k - 1]!
+
+/-- Prep for the pair ladder: parameter `k` selects `SD_k(x) · SD_k(x+1)`.
+Panics outside the registered `k = 1..5` schedule. -/
+def prepAdvSwinnertonDyerPair (k : Nat) : ZPoly :=
+  advSwinnertonDyerPair k
+
+/-- Prep for the block ladder: parameter `m` selects `∏_{i<m} SD_4(x+i)`. -/
+def prepAdvSwinnertonDyerSD4Blocks (m : Nat) : ZPoly :=
+  advSwinnertonDyerSD4Blocks m
+
+/--
+Ladder benchmark target: public factorization across the Swinnerton-Dyer
+ladder `SD_1 … SD_5`. Returns the canonical (order-insensitive) factor-multiset
+checksum so per-rung values can be checked offline against the
+`runIsabelleAdvSwinnertonDyer*` comparator rungs.
+-/
+@[noinline]
+def runFactorAdvSwinnertonDyerLadderChecksum (f : ZPoly) : UInt64 :=
+  checksumCanonicalLeanFactorization (factor f)
+
+/-- Ladder benchmark target: public factorization across `SD_k(x) · SD_k(x+1)`. -/
+@[noinline]
+def runFactorAdvSwinnertonDyerPairChecksum (f : ZPoly) : UInt64 :=
+  checksumCanonicalLeanFactorization (factor f)
+
+/-- Ladder benchmark target: public factorization across `∏_{i<m} SD_4(x+i)`. -/
+@[noinline]
+def runFactorAdvSwinnertonDyerSD4BlocksChecksum (f : ZPoly) : UInt64 :=
+  checksumCanonicalLeanFactorization (factor f)
+
 /-- Benchmark target: public combinator over the degree/height matrix. -/
 def runFactorDegreeHeightChecksum (input : DegreeHeightInput) : UInt64 :=
   checksumFactorization (factor input.poly)
@@ -748,6 +863,46 @@ def runIsabelleAdvSwinnertonDyerSD3Checksum : Unit → IO UInt64 := fun _ => do
   let (scalar, factors) ← requestIsabelleBZFactorization advSwinnertonDyerSD3
   return checksumCanonicalFactorization scalar factors
 
+/--
+Per-rung verified-Isabelle comparator targets for the Swinnerton-Dyer
+tier-crossover ladders (`runFactorAdvSwinnertonDyer{Ladder,Pair,SD4Blocks}Checksum`).
+One fixed registration per rung not already covered (`SD_1`–`SD_3` are covered
+by `runIsabelleFactorChecksum`/`runIsabelleAdvSwinnertonDyerSD3Checksum`;
+the pair rung `k = 4` and the block rung `m = 2` share one input).
+
+The pair rung `k = 5` (`SD_5(x)·SD_5(x+1)`) is deliberately absent: the AFP
+implementation has no lattice tier and its recombination exceeded a 120 s cap
+on the reference hardware (measured 2026-07-02), where hex's hybrid answers in
+~16 s. The headline report records it as the crossover, not as a rung.
+-/
+def runIsabelleAdvSwinnertonDyerSD4Checksum : Unit → IO UInt64 := fun _ => do
+  let (scalar, factors) ← requestIsabelleBZFactorization advSwinnertonDyerSD4
+  return checksumCanonicalFactorization scalar factors
+
+def runIsabelleAdvSwinnertonDyerSD5Checksum : Unit → IO UInt64 := fun _ => do
+  let (scalar, factors) ← requestIsabelleBZFactorization advSwinnertonDyerSD5
+  return checksumCanonicalFactorization scalar factors
+
+def runIsabelleAdvSwinnertonDyerPairK2Checksum : Unit → IO UInt64 := fun _ => do
+  let (scalar, factors) ← requestIsabelleBZFactorization (advSwinnertonDyerPair 2)
+  return checksumCanonicalFactorization scalar factors
+
+def runIsabelleAdvSwinnertonDyerPairK3Checksum : Unit → IO UInt64 := fun _ => do
+  let (scalar, factors) ← requestIsabelleBZFactorization (advSwinnertonDyerPair 3)
+  return checksumCanonicalFactorization scalar factors
+
+def runIsabelleAdvSwinnertonDyerPairK4Checksum : Unit → IO UInt64 := fun _ => do
+  let (scalar, factors) ← requestIsabelleBZFactorization (advSwinnertonDyerPair 4)
+  return checksumCanonicalFactorization scalar factors
+
+def runIsabelleAdvSwinnertonDyerSD4BlocksM3Checksum : Unit → IO UInt64 := fun _ => do
+  let (scalar, factors) ← requestIsabelleBZFactorization (advSwinnertonDyerSD4Blocks 3)
+  return checksumCanonicalFactorization scalar factors
+
+def runIsabelleAdvSwinnertonDyerSD4BlocksM4Checksum : Unit → IO UInt64 := fun _ => do
+  let (scalar, factors) ← requestIsabelleBZFactorization (advSwinnertonDyerSD4Blocks 4)
+  return checksumCanonicalFactorization scalar factors
+
 /--
 Per-rung verified-Isabelle BZ comparator targets on the cascade-trigger
 `prepFallbackProbeInput n = (X-1)(X-2)...(X-n)` family for each rung of
@@ -1185,6 +1340,76 @@ setup_benchmark runAdvSwinnertonDyerSD3ModularSplitChecksum n => n + 1
     signalFloorMultiplier := 1.0
   }
 
+/-
+Swinnerton-Dyer tier-crossover ladders (#8537 benchmark data, made tracked).
+
+Three one-parameter families over the public `factor`, all
+`scheduled-hardware` (the top rungs are multi-second lattice-tier runs, far
+past the `verify` budget). Verdicts on these families are not merge-gating;
+the scaling story lives in `reports/figures/hex-berlekamp-zassenhaus-sd-*.svg`
+(generated by `scripts/plots/hex-berlekamp-zassenhaus-sd.py` from the
+committed bench-results JSONL), and the per-rung canonical checksums are the
+regression signal.
+-/
+
+-- Cost-model derivation: `SD_k` splits into `r = 2^(k-1)` local factors mod
+-- every prime, and the classical tier certifies irreducibility only after
+-- enumerating its full head-forced subset powerset, `∑_d C(r-1, d) = 2^(r-1)`
+-- candidates; per-candidate work is polynomial in the degree, so the
+-- candidate count `2^(2^(k-1))` dominates and is the declared model. Five
+-- custom rungs cannot fit a doubly-exponential slope cleanly, so the verdict
+-- is expected inconclusive; the figures and checksums carry the signal.
+setup_benchmark runFactorAdvSwinnertonDyerLadderChecksum k => 2 ^ (2 ^ (k - 1))
+  with prep := prepAdvSwinnertonDyerLadder
+  where {
+    paramFloor := 1
+    paramCeiling := 5
+    paramSchedule := .custom #[1, 2, 3, 4, 5]
+    maxSecondsPerCall := 30.0
+    targetInnerNanos := 100000000
+    signalFloorMultiplier := 1.0
+    tags := #[scheduledHardwareTag]
+  }
+
+-- Cost-model derivation: for `k ≤ 4` the classical tier finds the two
+-- `2^(k-1)`-blocks within its subset budget, worst-case bounded by the same
+-- `2^(2^(k-1))`-shaped powerset enumeration as the irreducible ladder; at
+-- `k = 5` the winning size-16 subsets sit `∑ C(31, ≤15) ≈ 2^30` candidates
+-- deep, so classical declines at its level-aware boundary (a budget constant)
+-- and the polynomial CLD lattice tier answers — the declared doubly
+-- exponential model over-bounds that top rung, and no single textbook
+-- exponent fits across the tier crossover (verdict expected inconclusive).
+setup_benchmark runFactorAdvSwinnertonDyerPairChecksum k => 2 ^ (2 ^ (k - 1))
+  with prep := prepAdvSwinnertonDyerPair
+  where {
+    paramFloor := 1
+    paramCeiling := 5
+    paramSchedule := .custom #[1, 2, 3, 4, 5]
+    maxSecondsPerCall := 60.0
+    targetInnerNanos := 100000000
+    signalFloorMultiplier := 1.0
+    tags := #[scheduledHardwareTag]
+  }
+
+-- Cost-model derivation: `r = 8m` local factors. In the classical regime
+-- (`m ≤ 2`) the worst-case burn is the powerset bound `2^(8m - 1)`, so the
+-- declared model is `2^(8m)`; from `m = 3` classical declines at its
+-- level-aware budget boundary (a constant) and the polynomial CLD lattice
+-- tier dominates, which the declared exponential over-bounds — as with the
+-- pair ladder, no single textbook exponent fits across the crossover
+-- (verdict expected inconclusive).
+setup_benchmark runFactorAdvSwinnertonDyerSD4BlocksChecksum m => 2 ^ (8 * m)
+  with prep := prepAdvSwinnertonDyerSD4Blocks
+  where {
+    paramFloor := 1
+    paramCeiling := 4
+    paramSchedule := .custom #[1, 2, 3, 4]
+    maxSecondsPerCall := 120.0
+    targetInnerNanos := 100000000
+    signalFloorMultiplier := 1.0
+    tags := #[scheduledHardwareTag]
+  }
+
 /- Fixed bottom-rung verified-Isabelle comparator pair. Both targets return the
 same canonical factor-multiset checksum for `(x^2 - 2)(x^2 - 3)`; scheduled runs use
 `compare runFactorIsabelleDomainChecksum runIsabelleFactorChecksum` to record
@@ -1445,6 +1670,53 @@ setup_fixed_benchmark runIsabellePrecisionLocalRung6Checksum where {
     tags := #[scheduledHardwareTag]
   }
 
+-- Verified-Isabelle rungs for the Swinnerton-Dyer tier-crossover ladders.
+-- `expectedHash := none` per the fallback-probe precedent: computing the Lean
+-- reference checksum at elaboration time would run multi-second `factor`
+-- calls during compilation. Multiset agreement with the Lean rungs is checked
+-- offline in the headline report.
+setup_fixed_benchmark runIsabelleAdvSwinnertonDyerSD4Checksum where {
+    repeats := 3
+    maxSecondsPerCall := 60.0
+    tags := #[scheduledHardwareTag]
+  }
+
+setup_fixed_benchmark runIsabelleAdvSwinnertonDyerSD5Checksum where {
+    repeats := 3
+    maxSecondsPerCall := 60.0
+    tags := #[scheduledHardwareTag]
+  }
+
+setup_fixed_benchmark runIsabelleAdvSwinnertonDyerPairK2Checksum where {
+    repeats := 3
+    maxSecondsPerCall := 60.0
+    tags := #[scheduledHardwareTag]
+  }
+
+setup_fixed_benchmark runIsabelleAdvSwinnertonDyerPairK3Checksum where {
+    repeats := 3
+    maxSecondsPerCall := 60.0
+    tags := #[scheduledHardwareTag]
+  }
+
+setup_fixed_benchmark runIsabelleAdvSwinnertonDyerPairK4Checksum where {
+    repeats := 3
+    maxSecondsPerCall := 60.0
+    tags := #[scheduledHardwareTag]
+  }
+
+setup_fixed_benchmark runIsabelleAdvSwinnertonDyerSD4BlocksM3Checksum where {
+    repeats := 3
+    maxSecondsPerCall := 60.0
+    tags := #[scheduledHardwareTag]
+  }
+
+setup_fixed_benchmark runIsabelleAdvSwinnertonDyerSD4BlocksM4Checksum where {
+    repeats := 3
+    maxSecondsPerCall := 120.0
+    tags := #[scheduledHardwareTag]
+  }
+
 end BerlekampZassenhausBench
 end Hex
 

progress/20260702T120303Z_bench-sd-review.md

@@ -0,0 +1,20 @@
+**Accomplished**
+- Reviewed the `bench-sd-families` branch changes around the Swinnerton-Dyer
+  benchmark families, the SD figure generators, committed bench exports, and
+  the headline report section.
+- Checked the `scheduled-hardware` tag path through `hexbz_bench verify` and
+  CI's bench verify invocation.
+- Verified the report's listed SHA-256 values against the committed SD JSON
+  exports.
+
+**Current frontier**
+- The main review findings are packaging/traceability issues in the report and
+  figure scripts, plus one low-risk maintainability issue in the Lean prep
+  fallbacks.
+
+**Next step**
+- Fix the report/figure traceability issues before merging; the Lean
+  registrations and CI filter look structurally sound.
+
+**Blockers**
+- None.

progress/20260702T121500Z_bench-sd-families.md

@@ -0,0 +1,41 @@
+# bench-sd-families — SD tier-crossover ladders, figures, report
+
+Follow-up to PR #8537 (level-aware decline boundary), turning that PR's
+ad-hoc benchmark comments into tracked lean-bench targets with committed
+artefacts and figures, per Kim's request.
+
+**Accomplished**
+- Registered three one-parameter families in
+  `bench/HexBerlekampZassenhaus/Bench.lean` (all `scheduled-hardware`,
+  so merge-gating `verify` is unchanged — measured 18 targets / 0.04 s):
+  `SD_k` ladder (k = 1..5), pair ladder `SD_k(x)·SD_k(x+1)` (k = 1..5,
+  classical → lattice at k = 5), block ladder `∏_{i<m} SD_4(x+i)`
+  (m = 1..4, crossover at m = 3). SD literals pinned from sympy;
+  derived products via `DensePoly.compose`/mul with `#guard` pins of
+  constant coefficients. Seven new verified-Isabelle fixed rungs (every
+  rung the AFP extraction answers under 120 s; the pair k = 5 rung is
+  deliberately absent — no lattice tier, > 120 s).
+- Clean-tree exports committed under
+  `reports/bench-results/hex-berlekamp-zassenhaus-7da4747e-*.json`
+  (hex three families, Isabelle rungs incl. per-request baseline,
+  informational FLINT curve).
+- Figure generators `scripts/plots/hex-berlekamp-zassenhaus-sd.py`
+  (+ `-sd-flint.py`); three log-y SVGs in `reports/figures/`. The pair
+  figure shows the story in one glance: the verified reference's curve
+  leaves the chart at k = 5 where hex's lattice tier answers in 16.7 s.
+- Headline-report subsection (tables, artefact SHA-256s, agreement
+  hashes for all nine shared rungs — all AGREE — and trend narrative).
+
+**Current frontier**
+- Trend worth watching (recorded in the report as an optimisation
+  target): hex loses ground to the verified Isabelle extraction as `r`
+  grows on the pure certification ladder (hex/Isabelle ≈ 1.6 at SD4,
+  ≈ 10 at SD5) — the classical tier's full-powerset certification burn.
+
+**Next step**
+- Wire these families into whatever scheduled-hardware timing runs get
+  set up (SPEC §Scientific timing runs); the report records the exact
+  commands.
+
+**Blockers**
+- None.