feat(hex-roots): add bench/HexRoots/Bench.lean and CI wiring#8747
Merged
Conversation
Register the Phase 4 benchmark surface for the certified complex-root isolation library: the exact Gaussian-dyadic primitives (taylor, the two atom-witness checks, newtonSquare), mahlerPrec, the refinement primitives (refine1, certify?), the whole-polynomial drivers (isolateAll? at target 32, isolate to the separationDepth floor), refineTo?, and the sameRoot identity test, plus the dual-route atom-certificate compare group (isolate under .nk, .pellet, .nkThenPellet on a shared integer-root domain, joined on a strategy-invariant integer-grid projection of the isolation output). Wire the hexroots_bench exe into lakefile.lean, HEX_EXE_TARGETS, and the Bench verify step. Each setup_benchmark declares the textbook exact-dyadic-operation-count model from the SPEC complexity contract with an adjacent derivation comment; the declared models are op counts, not wall-time-with-bit-length models, so the scientific wall-time verdicts and their reconciliation are a scheduled-hardware concern as for the other Phase 4 benches. mahlerPrec is declared linear in degree because the seeded family holds the coefficient height fixed, reducing the O(n log||p||) contract to O(n) over the schedule. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01SpYSH4swVcLJbN2Bn6NfSP
The 2^-8 grid put bucket boundaries within reach of non-integer centres in principle; the compare family's roots are integers and every certified centre is within its square's radius of a root, so nearest-integer rounding is robustly strategy-invariant. Found by the Codex review. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01SpYSH4swVcLJbN2Bn6NfSP
scripts/check_phase4.py requires the cost-model derivation comment adjacent to each setup_benchmark registration: each compare-group registration now carries its own O(n^3) derivation (n rounds of O(n) witness checks at O(n) exact-dyadic ops on the fixed-height linProdPoly family). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01SpYSH4swVcLJbN2Bn6NfSP
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 adds the Phase 4 benchmark root
bench/HexRoots/Bench.lean(exehexroots_bench) for the certified complex-root isolation library, and wires it intolakefile.lean, the CIHEX_EXE_TARGETSset, and theBench verifystep. It registers the SPEC API surface with textbook exact-dyadic-operation-count complexity models and adjacent cost-model derivation comments:taylorand the two atom-witness checks (witnessCheck,nkWitnessCheck) at O(n²);newtonSquareat O(n²);mahlerPrecat O(n·log‖p‖∞) reduced to O(n) over a fixed-height family; the refinement primitivesComponent.refine1andComponent.certify?on a mid-refinement component; the whole-polynomial driversisolateAll?(target 32) andisolate(to theseparationDepthfloor) at O(n³);DyadicRootIsolation.refineTo?parametric in the target precision at O(t²); theRefinedIsolation.sameRootidentity test as a fixed microsecond benchmark; and the dual-route atom-certificatecomparegroup (isolateunder.nk,.pellet,.nkThenPellet) over a shared∏(X−j)integer-root domain, joined on a strategy-invariant integer-grid projection of the isolation output.Two deterministic input families key on the benchmark parameter (its degree): a seed-
0xC0FFEELCG dense family matching the conformance ci-tier fixtures (irrational distinct roots, used bytaylor/mahlerPrec/the refinement primitives/the two drivers), and the Wilkinson-shapedlinProdPolyproduct of distinct monic linears (integer roots, used by the witness/Newton registrations centred on root1and by thecomparegroup, where the exact integer centres make the three strategies' digests agree). Helper defs not in the SPEC:lcgNext/seededCoeffs/seededPoly/linProdPoly/linearFactor(input families),taylorCentre/rootSquare/refinePoly(fixtures),midComponent(the certify?/refine1 fixture),refineAtom?/refinedAtom?(the refineTo?/sameRoot fixtures), the*Checksum/rootsDigest/gridBucket/bucketLeobservables, andHashableinstances forZPoly/DyadicSquare/Component/DyadicRootIsolationrouting through the exact-rational observables.Deviation from the canonical textbook complexity: the declared models are exact-dyadic-operation counts (per the SPEC complexity contract's "O(n²) exact-dyadic operations on B-bit values" phrasing); they do not fold in the working bit-length
B = prec + n·log‖p‖∞, which grows with the parameter, so the scientific wall-time verdicts run inconclusive with a positive residual slope on this hardware and are reconciled on scheduled hardware, consistent with the other Phase 4 benches.mahlerPrecis declared O(n) because the seeded family holds‖p‖∞ ≤ 10fixed.Verification on this machine (Lean 4.32.0-rc1):
lake build hexroots_benchgreen;lake exe hexroots_bench listshows all 14 registrations;lake exe hexroots_bench verifypasses all 14 in ~0.7 s wallclock (well under the 30 s soft warning and 360 s hard cap);python3 scripts/ci/check_benches_mathlib_free.pypasses (no bench reaches Mathlib);compareover the three strategies reports "all functions agree on common params". Spot-checkedisolateAll?timings stay under the 20 s per-call cap with no killed rows (58 ms at degree 8, 484 ms at degree 12, 4 s at degree 20; the full ladder runs in ~15 s), so no scientific settings were weakened to fit any budget.🤖 Prepared with Claude Code