bench: Swinnerton-Dyer tier-crossover ladders with scaling figures#8539
Open
kim-em wants to merge 7 commits into
Open
bench: Swinnerton-Dyer tier-crossover ladders with scaling figures#8539kim-em wants to merge 7 commits into
kim-em wants to merge 7 commits into
Conversation
…blocks) Register the #8537 benchmark families as tracked lean-bench targets: the SD_k irreducible ladder (k = 1..5), the pair ladder SD_k(x)*SD_k(x+1) (k = 1..5, classical -> lattice crossover at k = 5), and the block ladder prod_{i<m} SD_4(x+i) (m = 1..4, crossover at m = 3), plus verified-Isabelle comparator rungs for every rung the AFP implementation can answer under a 120 s cap (measured: all but the pair k = 5, where its latticeless recombination exceeds 120 s and hex's hybrid answers in ~16 s). SD literals are pinned from sympy minimal_polynomial; derived products go through DensePoly.compose/mul with #guard pins of their constant coefficients against the sympy expansion, so an arithmetic regression cannot silently change the inputs. All registrations are tagged scheduled-hardware: verify (and hence merge-gating CI) skips them. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Add scripts/plots/hex-berlekamp-zassenhaus-sd.py (three log-y wall-time figures from the committed lean-bench exports, with the Isabelle per-request baseline subtracted per the headline-report convention and missing comparator rungs annotated rather than dropped) and the companion hex-berlekamp-zassenhaus-sd-flint.py (informational python-flint curve, inputs cross-checked against the Lean #guard pins). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Clean-tree lean-bench exports for the three SD families and the verified-Isabelle rungs, the informational python-flint curve, and the three generated log-y scaling figures. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Tables, figures, artefact SHA-256s, hex-vs-Isabelle multiset-agreement hashes for all nine shared rungs, and the trend narrative (including the hex-loses-ground-with-r observation on the certification ladder, flagged as an optimisation target). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Commit the sd4-blocks figure the earlier glob missed; map the SD4 measurement onto the blocks m=1 comparator point; make the plot script refuse to guess between multiple committed sweeps and drop (with a warning) baseline-limited Isabelle rungs instead of plotting artificial points; add degree asserts and a scope note to the FLINT cross-check; make the ladder preps panic loudly out of schedule instead of silently substituting SD3; state the eight-distinct-inputs/two-duplications structure of the agreement hashes explicitly in the report. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Cost-model derivation, per family: SD_k splits into r = 2^(k-1) local factors mod every prime and classical certification enumerates the full head-forced subset powerset, so the candidate count 2^(2^(k-1)) dominates and is the declared complexity model for the ladder; the pair family is bounded by the same worst-case powerset shape through k = 4 and by the budget-constant decline plus the polynomial CLD lattice tier at k = 5; the block family's classical regime is the powerset bound 2^(8m - 1), declared 2^(8m), with the same polynomial lattice dominance past the m = 3 crossover. No single textbook exponent fits across a tier crossover, so the top-rung verdicts are expected inconclusive; the committed figures and per-rung canonical checksums carry the regression signal. Replaces the k + 1 placeholders that scripts/check_phase4.py rightly rejected as not being cost-model derivations. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Re-sweep after the cost-model derivation commit so the committed artefacts, figures, and the headline report all cite one commit. All ten Isabelle-covered rows keep their canonical factor-multiset hashes (agreement unchanged); the trend-narrative ratios are now consistently overhead-adjusted (hex/Isabelle ~3.8 at SD4, ~9.5 at SD5 on the certification ladder). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This PR turns the benchmark data recorded on #8537 "perf: level-aware classical decline boundary" into tracked lean-bench targets with committed artefacts and scaling figures. Three one-parameter families over the public
factorregister inbench/HexBerlekampZassenhaus/Bench.lean: the Swinnerton-Dyer ladderSD_k(k = 1..5, irreducible worst cases), the pair ladderSD_k(x)·SD_k(x+1)(k = 1..5, classical → lattice crossover at k = 5), and the block ladder∏_{i<m} SD_4(x+i)(m = 1..4, crossover at m = 3), plus seven verified-Isabelle comparator rungs — every rung the AFPBerlekamp_Zassenhausextraction answers under a 120 s cap (the pair k = 5 rung is deliberately absent: the AFP implementation has no lattice tier and exceeds the cap, where hex's hybrid answers in 16.7 s). SD literals are pinned from sympyminimal_polynomial; the derived pair/block products go throughDensePoly.compose/*with#guardpins of their constant coefficients, so an arithmetic regression cannot silently change the inputs. Everything is taggedscheduled-hardware: merge-gatingverifyis byte-for-byte unchanged (18 targets, 0.04 s).Clean-tree exports are committed under
reports/bench-results/hex-berlekamp-zassenhaus-7da4747e-*.json, andscripts/plots/hex-berlekamp-zassenhaus-sd.py(with the-sd-flint.pycompanion for the informational FLINT curve) generates three log-y wall-time figures inreports/figures/, one per family, with the Isabelle per-request baseline subtracted and off-scale comparator rungs drawn as a rising tail rather than dropped. The headline report gains a "Swinnerton-Dyer tier-crossover ladders" subsection with the tables, artefact SHA-256s, the trend narrative, and the canonical factor-multiset hashes on which hex and the verified Isabelle extraction agree at all nine shared rungs — the per-rung regression signal for future sweeps. The narrative also records the adverse trend on the pure certification ladder (hex/Isabelle grows from ≈ 1.6 at SD4 to ≈ 10 at SD5, the classical tier's full-powerset certification burn) as an optimisation target.🤖 Prepared with Claude Code