perf: build the disambiguation eliminant as a double resultant - #9432
Merged
Conversation
kim-em
enabled auto-merge (squash)
August 22, 2026 08:43
This was referenced Aug 26, 2026
kim-em
force-pushed
the
wave/roots-refinement-fix
branch
from
August 26, 2026 01:01
07335af to
7034911
Compare
…luation eliminant QAdjoin.Roots.evalRoot? built each candidate's disambiguation eliminant by exact lazy AlgebraicRoot Horner arithmetic: every intermediate mul?/add? re-isolated all roots of an intermediate eliminant whose degree multiplied by deg(candidate.p) at each step, so a rung-2 root-ladder call exceeded 20 minutes against a 26 ms rung 1. Replace that chain with one integer eliminant per component, QAdjoin.Roots.evalEliminant: the double resultant Res_y(p(y), Res_z(e(z), S - G(y, z))) with G = clearedOuter f and e the component's squarefree norm-eliminant core, dilated by the common denominator so its roots are the candidate evaluation values themselves. Its degree is deg(p) * deg(e) (8 at ladder rung 2, versus 51 for the old per-candidate chain), heights are Hadamard-bounded, and no root isolation happens on the evaluation side. The bounded search retainZero? / evalDisambiguationPrec / evalBall? is unchanged and still performs the SPEC's remove-maximal-X-power plus primitive-part normalization internally; componentRoots? now feeds it the shared evaluation eliminant. candidateLift and evalShifted are the trivariate resultant inputs, built in the clearedOuter style. evalRoot? and its only consumer coeffRoot? are deleted (the companion lemma rebuild follows in the next commit). Root-ladder timings on chungus2 (runQAdjoinRootsLadder): rung 1 26 ms -> 3.9 ms, rung 2 >20 min (killed) -> 128 ms, rung 3 1.19 s, rung 4 7.9 s, rung 6 105.7 s; runAlgebraicRootsLadder rungs 2-6: 50 ms / 149 ms / 0.71 s / 6.2 s. A compiled #guard pins the S^2(S^2 - 8) eliminant for X - sqrt2 over Q(sqrt2). Progress: progress/2026-08-21T06-33-46Z.md (previous turn) Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…on eliminant Replace the deleted evalRoot? lemma cluster (coeffRoot?_isSome/_sound, evalRootFold_*, evalRoot?_isSome/_sound) with the two facts the bounded zero test consumes about the new eliminant, both in HexNumberFieldMathlib/Roots.lean: - evalEliminant_isRoot: the true evaluation value is a root, via a hom-generic private resultant_hom_eq_zero for the inner Res_z(e, S - G) layer (over a proof-local CommRing/IsDomain on DensePoly ZPoly), the existing resultant_isRoot for the outer layer, clearedOuter_eval for the specialization identity, and a dilation transport toPolyC_dilate_isRoot. - evalEliminant_ne_zero: choose a specialization value outside the finite set of cleared-lift evaluations at root pairs; both resultant layers are then coprime specializations with nonvanishing leading-coefficient padding, mirroring normEliminant_ne_zero. Supporting lemmas: coeff/size characterizations of candidateLift and evalShifted, the specialization identities candidateLift_map and evalShifted_map_eval (the transposed double-sum mirror of clearedOuter_evalAt), one_lt_size_liftOuter, and size_pos_of_core_degree (a positive-degree squarefree core forces a nonzero component, so componentRoots?_sound/_complete need no new hypotheses). retainZero?_correct now takes the shared evaluation eliminant directly; componentRoots?_isSome/_sound/_complete drop the evalRoot? bind. All 23 companion axiom guards pass, with the evalRoot?_sound guard replaced by one on retainZero?_correct. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
With the double-resultant evaluation eliminant in place, the shipped runQAdjoinRootsLadder schedule [1, 2, 3, 4, 6] measures 3.9 ms / 128 ms / 1.17 s / 7.9 s / 105.4 s per call on chungus2 (before the fix, rung 2 alone exceeded 20 minutes and was killed). The declared n^5 log^2 n model predicts rung 6 at about 17x rung 4 (6^5 * log2(8)^2 / (4^5 * log2(6)^2) = 69984/16384), i.e. ~134 s against the old 60 s cap, and the measured 105 s confirms the cap, not the model, was the binding constraint. 180 s leaves ~70% headroom over the measured rung-6 time so the scientific schedule completes on the timing hardware; the declared model line is unchanged. Sibling runAlgebraicRootsLadder needs no change (6.2 s at its top rung against its existing 60 s cap). Fixes measured against the rung fixtures of issue #9423; the diagnostic session's reference timings were rung 1 = 26 ms, rung 2 > 20 min. Progress: progress/2026-08-22T08-39-56Z.md Closes #9423 Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
kim-em
force-pushed
the
wave/roots-refinement-fix
branch
from
August 26, 2026 01:31
bf68471 to
511750b
Compare
Add a non-unit-denominator guard for the shared double resultant, make the SPEC's per-component construction explicit, and account for its linear evaluation-variable degree in the root-ladder derivation.
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 fix the exponential eliminant growth that #9423's root-cause analysis located in
QAdjoin.Roots.evalRoot?: the disambiguation eliminant was assembled by per-candidate lazy Horner arithmetic, multiplying eliminant degree at every step and dragging dead root-isolation work along (one intermediatemul?at the smallest irrational rung exceeded twenty minutes). The replacement computes one shared evaluation eliminant per component as the double resultantRes_y(p(y), Res_z(e(z), S - G(y,z)))withG = clearedOuter f, dilated by the common denominator, exactly as SPEC §Polynomial roots step 4 words it;retainZero?,evalDisambiguationPrec, andevalBall?are unchanged,evalRoot?and its sole consumer are deleted, and a compiled#guardpins theS^2(S^2-8)eliminant forX - sqrt 2overQ(sqrt 2). The companion rebuilds the affected surface:evalEliminant_isRootandevalEliminant_ne_zeroin the norm-eliminant style,retainZero?_correctrestated against the shared eliminant, and thecomponentRoots?soundness/completeness/totality proofs repaired, with all 23 axiom guards and 24 rfl pinning regressions passing and zero sorries. Rung timings move from 26 ms / killed-past-twenty-minutes at rungs 1/2 to 3.9 ms / 128 ms / 1.17 s / 7.9 s / 105.4 s at rungs 1/2/3/4/6, and the algebraic-poly ladder reads faster than its declared model; the QAdjoin roots ladder's per-call cap widens 60 to 180 s with the derivation in the commit body, its declared model unchanged.Closes #9423
🤖 Prepared with Claude Code