bench: add the number-field pair's Phase-4 ladders, PARI comparator, and declarations - #9424
Merged
Conversation
kim-em
enabled auto-merge (squash)
August 22, 2026 06:49
kim-em
force-pushed
the
wave/number-field-phase4
branch
4 times, most recently
from
August 24, 2026 02:33
e02774b to
5d29b3d
Compare
This adds scripts/oracle/pari_bench_driver.py, a cypari2-backed persistent-subprocess bench driver following the shape of flint_bench_driver.py (one JSON request per line, error frames never fatal, interpreter constructed once at startup), and Hex/BenchOracle/Pari.lean, the Lean-side helper reusing the Flint module's PersistentComparator plumbing with its own driver cache and HEX_PARI_BENCH_DRIVER / HEX_PARI_BENCH_PYTHON configuration. The driver exposes the polmod family (mul, inv, overhead) for arithmetic in Q[x]/(m) via PARI t_POLMOD, and the nf family (factor_degrees) wrapping nffactor and returning the sorted factor degree/multiplicity multiset. Rationals cross the protocol as normalised [num, den] pairs. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
… pairs This adds the parametric Phase-4 evidence for HexNumberField and HexNumberFieldTower, completes the tower arithmetic fixed surface (Sub/Neg/Div/SMul), and wires per-rung Lean/PARI comparator pairs through the persistent pari_bench_driver. Cost-model derivations for the added registrations (declared textbook complexity, independent of harness output): - runQAdjoinAddLadder: n. Coordinatewise rational addition of two reduced degree-(n-1) coefficient vectors is a linear number of O(1) rational operations at bounded fixture heights. - runQAdjoinMulLadder: n^2. Dense schoolbook multiplication is a quadratic number of coefficient operations; reduction modulo the sparse monic X^n - 2 retires O(n) coefficients at O(1) each, so the quadratic convolution dominates. - runQAdjoinInvLadder: n^2 log n. Polynomial extended gcd against the degree-n modulus over Q is a quadratic number of coefficient operations (SPEC complexity section); the Euclidean chain's coefficient growth is modelled with the logarithmic limb-growth proxy used by the HexResultant Brown-chain registrations. - runAddEliminantLadder: n^2 log n. The Brown resultant of a degree-n constant-coefficient polynomial against the monic y-quadratic (t - y)^2 - 3 performs O(n) monic elimination steps on remainders whose t-degrees grow to O(n), a quadratic number of integer coefficient operations, with the same logarithmic limb proxy. - runLazyAddLadder: n^5 log^2 n. Per the SPEC, the lazy binary ceiling is resultant cost plus root isolation at the eliminant degree d = 2n, and separation-depth isolation dominates: with the HexRoots heuristic O(d^3 B^2) and tau, B = O(d log d) from the resultant Hadamard bound, the wall shape is d^5 log^2 d. - runExactLadder: n^9 + n^7 log^2 n. Exactification adds one Berlekamp-Zassenhaus factorization of the enclosing polynomial; the classical BHKS bound in the enclosing degree dominates the candidate re-isolation and canonicalization. - runQAdjoinRootsLadder / runAlgebraicRootsLadder: n^5 log^2 n. The root APIs run Yun decomposition (quadratic, lower order) and one norm eliminant per squarefree component; the degree-2n eliminant's separation-depth isolation dominates exactly as in the lazy-add derivation. - runCommonPresentationLadder: n. With one quadratic irrational among n rational coefficients, primitive? tests a constant number of shifts per coefficient and coordinates? embeds each coefficient with a constant number of degree-2 trace-pairing operations, so the common-field construction is a linear number of constant-size canonical operations. - runTowerAddLadder: n. Coordinate addition visits exactly D = 2n mixed-radix rational coordinates (SPEC: O(D)). - runTowerMulLadder: n^2. Schoolbook convolution plus top-down monic reduction is O(D^2) rational operations (SPEC: O(D^2)). - runTowerInvLadder: n^2 log n. Extended gcd in the top quotient of relative degree n over the fixed quadratic base is a quadratic number of base-field operations, with the logarithmic limb proxy for Euclidean coefficient growth. - runTowerFactorLadder: tragerLadderModel n, the SPEC's worst-case shift recurrence written out: at most choose(2n, 2) + 1 one-level norms, each an O(n^2)-operation Brown resultant against the quadratic level relation, plus the recursive rational factorization of the accepted degree-2n norm at its classical BHKS bound, which dominates. The PARI pairs (QAdjoin mul/inv vs t_POLMOD, factor? vs nffactor) are fixed per-rung process-call registrations per SPEC/benchmarking.md External comparators / Process call: both sides use warmupFirstIter so lazily built rung fixtures and the persistent driver spawn stay outside the timed region, and share the minTotalSeconds floor so ratios compare steady-state medians. Hash joins use the reduced rational coefficient vector (polmod) and the sorted factor degree/multiplicity multiset (nffactor). Verification note: lake exe hexnumberfield_bench verify and hexnumberfieldtower_bench verify pass; the ladder smoke params exercise the clamped smallest fixtures. Feasibility probing during development found that QAdjoin.roots? on a degree-2 component with an irrational coefficient (and hence AlgebraicPoly.roots? on the matching family) currently runs for minutes, dominated by exact dyadic refinement; the scientific rungs of the two root ladders are expected to surface this as a Phase-4 finding at measurement time. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…eld pair This adds External comparators sections to the hex-number-field and hex-number-field-tower SPECs and matching phase4 blocks in libraries.yml. PARI/GP via cypari2 is named and classified informational with a structural-gap rationale: it is a mature optimized C library, so its constant-factor advantage over the verified implementations is structural, not algorithmic. Its wired scope is real and per-rung: t_POLMOD arithmetic paired with QAdjoin multiplication and extended-gcd inversion (both quadratic coefficient-operation cost models), and nffactor paired with factor? on shared Selmer inputs (worst-case Trager shift-recurrence cost model). Surfaces PARI does not expose as callable units — lazy certified arithmetic, exactification, certified root sets, mixed-radix tower arithmetic, adjoining, splitting, flattening — are declared absent with the no-comparable-surface-in-named-comparator reason. The input_families entries mirror the bench families registered with the declared textbook complexity models. Progress: progress/2026-08-22T05-30-00Z.md Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Hex/BenchOracle/Pari.lean is comparator plumbing never imported by the factorization service or any Hex library module, so the recorded hex-factor sweep still covers the executable factorization source. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Szi3AHDr5fpM8rFBUNrZAq
kim-em
force-pushed
the
wave/number-field-phase4
branch
from
August 25, 2026 23:00
5d29b3d to
16a1acc
Compare
This was referenced Aug 26, 2026
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 add the Phase-4 evidence code for HexNumberField and HexNumberFieldTower: thirteen parametric
setup_benchmarkladders with adjacent cost-model derivations covering every declared input family, the missing TowerSub/Neg/Div/SMulfixed registrations so every SPEC-API operation is assigned to a track, a persistent PARI bench comparator driver (scripts/oracle/pari_bench_driver.py+Hex/BenchOracle/Pari.lean, reusing the Flint persistent-comparator plumbing) with warmed hash-joined Lean/PARI pairs fort_POLMODarithmetic andnffactor, and thephase4:blocks plus## External comparatorsSPEC sections for both libraries. Surfaces PARI does not expose as callable API (certified lazy arithmetic, exactification, the certified root sets, mixed-radix coordinates, fixed-embedding adjoin/split/flatten) are declaredno-comparable-surface-in-named-comparatorwith per-surface reasons.Performance-rationale paragraph per PLAN/Phase4.md: the exactification ladder declares the BHKS-shaped
n^9 + n^7 log^2bound rather than a smaller observed cost; the lazy-arithmetic and root ladders declaren^5 log^2degree-product envelopes (worst-case, not amortised); and the Tower's Trager ladder declares the SPEC's shift recurrence written out as(choose(2n,2)+1) n^2 + (2n)^9 + (2n)^7 log^2 (2n), with the SelmerX^n - X - 1overQ(sqrt 2)family chosen so every rung exercises the shift retry, the accepted squarefree norm, the recursive rational factorization, and gcd recovery rather than a best case. No timed measurements land here; feasibility probing found the fixed-field root path pathological at rung 2 (minutes against the declared model), filed as #9423 and blocking that surface's scientific rungs; the measurement/report/bump PR follows once the external measurement queue drains and #9423 resolves.🤖 Prepared with Claude Code