theorem HexRealRootsMathlib.aevalIff_radical {orig core a b : Hex.ZPoly} {t : ℤ} {k : ℕ} (ht : t ≠ 0) (h1 : ∀ (x : ℝ), (Polynomial.aeval x) (HexPolyZMathlib.toPolynomial orig) = (Polynomial.aeval x) (HexPolyZMathlib.toPolynomial core) * (Polynomial.aeval x) (HexPolyZMathlib.toPolynomial a)) (h2 : ∀ (x : ℝ), ↑t * (Polynomial.aeval x) (HexPolyZMathlib.toPolynomial core) ^ (k + 1) = (Polynomial.aeval x) (HexPolyZMathlib.toPolynomial a) * (Polynomial.aeval x) (HexPolyZMathlib.toPolynomial b)) (x : ℝ) : (Polynomial.aeval x) (HexPolyZMathlib.toPolynomial core) = 0 ↔ (Polynomial.aeval x) (HexPolyZMathlib.toPolynomial orig) = 0

Radical root-equivalence from a divisibility certificate. Given reified integer polynomials orig, core, a, b, a nonzero integer scalar t, and an exponent k, the two pointwise identities

• orig = core * a (so every root of core is a root of orig), and

• t · core ^ (k+1) = a * b (so every root of a is a root of core, since t ≠ 0 and ℝ has no zero divisors),

pin the real roots of orig and core to the same set. Used by the elaborator to transport a square-free-core isolation onto the original non-squarefree polynomial without ever reducing Hex.ZPoly.squareFreeCore.

def HexRealRootsMathlib.aevalRingEq : Lean.ParserDescr

Reconcile two closed reified polynomial evaluations aeval x (…) = aeval x (…) by expanding every aeval-of-ofCoeffs into its explicit coefficient sum and pushing aeval through the user polynomial's X / C / + / − / * / ^ / neg structure, then closing with ring. Deliberately avoids mul_eq_zero, so a factored user polynomial (e.g. Wilkinson) does not collapse into a root disjunction.

Equations

• HexRealRootsMathlib.aevalRingEq = Lean.ParserDescr.node `HexRealRootsMathlib.aevalRingEq 1024 (Lean.ParserDescr.nonReservedSymbol "aeval_ring_eq" false)

def HexRealRootsMathlib.aevalIffBridge : Lean.ParserDescr

Prove ∀ x, aeval x P = 0 ↔ aeval x Q = 0 for reified/closed literal polynomials by reducing to the underlying evaluation equality.

Equations

• HexRealRootsMathlib.aevalIffBridge = Lean.ParserDescr.node `HexRealRootsMathlib.aevalIffBridge 1024 (Lean.ParserDescr.nonReservedSymbol "aeval_iff_bridge" false)

def HexRealRootsMathlib.isolateRootsProd : Lean.ParserDescr

Bridge tactic for the reified product identities aevalIff_radical consumes.

Equations

• HexRealRootsMathlib.isolateRootsProd = Lean.ParserDescr.node `HexRealRootsMathlib.isolateRootsProd 1024 (Lean.ParserDescr.nonReservedSymbol "isolate_roots_prod" false)

def HexRealRootsMathlib.IsolateRoots.evalZPoly (e : Lean.Expr) : Lean.MetaM Hex.ZPoly

Evaluate a closed Hex.ZPoly expression to its runtime value at elaboration time (compiled evaluation, not kernel reduction).

Equations

• One or more equations did not get rendered due to their size.

def HexRealRootsMathlib.IsolateRoots.evalRat (e : Lean.Expr) : Lean.MetaM ℚ

Evaluate a closed Rat-typed (or ℚ) expression to a Rat at elaboration time (hoisted to HexPolyZMathlib.PolyParse).

Equations

• HexRealRootsMathlib.IsolateRoots.evalRat e = HexPolyZMathlib.PolyParse.evalRat "isolate_roots" e

def HexRealRootsMathlib.IsolateRoots.parsePoly (isRat : Bool) (fuel : ℕ) (e : Lean.Expr) : Lean.MetaM Hex.ZPoly

Recursive interpreter from a Polynomial R expression to a Hex.ZPoly value (hoisted to HexPolyZMathlib.PolyParse). isRat selects the ℚ-style non-integer rejection.

Equations

• HexRealRootsMathlib.IsolateRoots.parsePoly isRat fuel e = HexPolyZMathlib.PolyParse.parsePoly "isolate_roots" isRat fuel e

def HexRealRootsMathlib.IsolateRoots.powZ (base : Hex.ZPoly) (k : ℕ) : Hex.ZPoly

base ^ k for Hex.ZPoly, via the executable Mul (csimp to mulImpl).

Equations

• One or more equations did not get rendered due to their size.

def HexRealRootsMathlib.IsolateRoots.divExactInt (num den : Array ℤ) : Option (Array ℤ)

Exact long division of integer coefficient arrays (ascending degree), returning the quotient coefficients when the division is exact, else none.

Equations

• One or more equations did not get rendered due to their size.

structure HexRealRootsMathlib.IsolateRoots.IsoData : Type

The certified isolation data extracted at elaboration time: a reified polynomial (the square-free core, when a swap happened), its Sturm chain, and the per-root dyadic endpoints.

• poly : Hex.ZPoly

  The reified polynomial whose roots are isolated.

• chain : Array Hex.ZPoly

  The executable Sturm chain used to certify the result.

• endpoints : Array (Dyadic × Dyadic)

  One dyadic interval for each distinct real root.

def HexRealRootsMathlib.IsolateRoots.runBackend (f : Hex.ZPoly) (widthK : Option ℤ) : Lean.MetaM IsoData

Run the compiled isolator on f (assumed square-free with a nonzero constant Sturm tail), optionally refining every root to width 2 ^ (-widthK) through the cached-chain refineToWithChain.

Equations

• One or more equations did not get rendered due to their size.

def HexRealRootsMathlib.IsolateRoots.intStx (c : ℤ) : Lean.MetaM (Lean.TSyntax `term)

Term syntax for an Int literal.

Equations

• One or more equations did not get rendered due to their size.

def HexRealRootsMathlib.IsolateRoots.natStx (n : ℕ) : Lean.TSyntax `term

Term syntax for a Nat literal.

Equations

• HexRealRootsMathlib.IsolateRoots.natStx n = { raw := (Lean.Syntax.mkNumLit (toString n)).raw }

def HexRealRootsMathlib.IsolateRoots.zpolyStx (f : Hex.ZPoly) : Lean.MetaM (Lean.TSyntax `term)

Term syntax for a reified Hex.ZPoly as Hex.DensePoly.ofCoeffs #[…].

Equations

• One or more equations did not get rendered due to their size.

def HexRealRootsMathlib.IsolateRoots.dyadicStx (d : Dyadic) : Lean.MetaM (Lean.TSyntax `term)

Term syntax for a Dyadic endpoint as Dyadic.ofInt m or Dyadic.ofInt m >>> (s : Int) (the denominator is a power of two).

Equations

• One or more equations did not get rendered due to their size.

def HexRealRootsMathlib.IsolateRoots.emitOfCert (d : IsoData) : Lean.MetaM (Lean.TSyntax `term)

Emit the replay term IsolatedRealRoots.ofCert for d.poly (a square-free polynomial), stated over HexPolyZMathlib.toPolynomial d.poly. Every field is a decide on literals against the reified chain.

Equations

• One or more equations did not get rendered due to their size.

def HexRealRootsMathlib.IsolateRoots.widthTarget (q : ℚ) : Lean.MetaM ℤ

Convert a positive rational width q to the bit target k = max 0 ⌈log₂ q⁻¹⌉ in exact integer arithmetic: the least k ≥ 0 with 2 ^ (-k) ≤ q. Widths above 1 give k = 0 (they never coarsen the natural intervals).

Equations

• One or more equations did not get rendered due to their size.

def HexRealRootsMathlib.IsolateRoots.radicalCert (orig core : Hex.ZPoly) : Lean.MetaM (Hex.ZPoly × Hex.ZPoly × ℤ × ℕ)

Compute the divisibility certificate (a, b, t, k) witnessing that orig and core share their real roots: orig = core * a and t · core ^ (k+1) = a * b with t ≠ 0, all as integer-polynomial identities. Throws the internal certificate-mismatch error if the executable decomposition does not reassemble (a bug).

Equations

• One or more equations did not get rendered due to their size.

def HexRealRootsMathlib.IsolateRoots.emitIsolation (f : Hex.ZPoly) (widthK : Option ℤ) : Lean.MetaM (Lean.TSyntax `term)

Emit coreTerm : IsolatedRealRoots (toPolynomial fLit) n for the reflected integer polynomial f (the reflection of the user's input), classifying it as zero / nonzero constant / square-free / non-squarefree and routing accordingly.

Equations

• One or more equations did not get rendered due to their size.

def HexRealRootsMathlib.IsolateRoots.elabIsolate (widthStx : Option (Lean.TSyntax `term)) (pStx : Lean.TSyntax `term) (expectedType? : Option Lean.Expr) : Lean.Elab.TermElabM Lean.Expr

Shared driver for the isolate_roots term elaborator.

Equations

• One or more equations did not get rendered due to their size.

def HexRealRootsMathlib.IsolateRoots.isolateRoots : Lean.ParserDescr

isolate_roots p / isolate_roots (width := x) p. The atomic lookahead on "(" "width" ":=" lets a parenthesised polynomial argument (e.g. (X^4 - 2 : Polynomial ℝ)) parse as the polynomial rather than the width group.

Equations

• One or more equations did not get rendered due to their size.

def HexRealRootsMathlib.IsolateRoots.elabIsolateRoots : Lean.Elab.Term.TermElab

Elaborate isolate_roots, run the compiled search, and emit a replay term whose certificate obligations are checked by Lean.

Equations

• One or more equations did not get rendered due to their size.