structure Hex.IsolatedRealRoots {R : Type u_1} [CommRing R] [Algebra R ℝ] (P : Polynomial R) (n : ℕ) : Type

A complete, certified real-root isolation of P : Polynomial R over ℝ: n rational intervals, each holding exactly one real root, together covering every real root, sorted and pairwise disjoint. Props are in aeval form so the same structure serves R = ℤ (a Hex.ZPoly via HexPolyZMathlib.toPolynomial), R = ℚ, and R = ℝ.

• intervals : Vector (ℚ × ℚ) n

  The n isolating intervals (lower, upper], as pairs of rationals.

• unique_root (i : Fin n) : ∃! x : ℝ, (Polynomial.aeval x) P = 0 ∧ ↑self.intervals[i].1 < x ∧ x ≤ ↑self.intervals[i].2

  Each interval holds exactly one real root of P.

• covers (x : ℝ) : (Polynomial.aeval x) P = 0 → ∃ (i : Fin n), ↑self.intervals[i].1 < x ∧ x ≤ ↑self.intervals[i].2

  Every real root of P lies in one of the intervals.

• ordered (i j : Fin n) : i < j → self.intervals[i].2 ≤ self.intervals[j].1

  The intervals are sorted and pairwise disjoint: the upper endpoint of each is at most the lower endpoint of every later one. With half-open intervals this makes n exactly the number of distinct real roots.

noncomputable def Hex.IsolatedRealRoots.congrRoots {R : Type u_1} {S : Type u_2} [CommRing R] [Algebra R ℝ] [CommRing S] [Algebra S ℝ] {P : Polynomial R} {Q : Polynomial S} {n : ℕ} (h : ∀ (x : ℝ), (Polynomial.aeval x) P = 0 ↔ (Polynomial.aeval x) Q = 0) : IsolatedRealRoots P n → IsolatedRealRoots Q n

Transport an isolation along a pointwise root equivalence. One lemma, used twice by the elaborator: the squarefree-core step and the user-polynomial step. Heterogeneous in the coefficient ring, since the structure only sees P through aeval x P = 0.

Equations

• Hex.IsolatedRealRoots.congrRoots h H = { intervals := H.intervals, unique_root := ⋯, covers := ⋯, ordered := ⋯ }

@[simp]

theorem Hex.IsolatedRealRoots.congrRoots_intervals {R : Type u_1} {S : Type u_2} [CommRing R] [Algebra R ℝ] [CommRing S] [Algebra S ℝ] {P : Polynomial R} {Q : Polynomial S} {n : ℕ} (h : ∀ (x : ℝ), (Polynomial.aeval x) P = 0 ↔ (Polynomial.aeval x) Q = 0) (H : IsolatedRealRoots P n) : (congrRoots h H).intervals = H.intervals

congrRoots leaves the intervals untouched, so simp reduces a transported isolation's intervals to the underlying ones.

def Hex.IsolatedRealRoots.constant {R : Type u_1} [CommRing R] [Algebra R ℝ] {c : R} (hc : (algebraMap R ℝ) c ≠ 0) : IsolatedRealRoots (Polynomial.C c) 0

The n = 0 result for a constant whose real image is nonzero: it has no real roots, so the empty isolation is complete. Nonzero constants never enter the isolator (the squarefree Sturm certificate is false on constants by design), so the elaborator dispatches them here.

Equations

• Hex.IsolatedRealRoots.constant hc = { intervals := #v[], unique_root := ⋯, covers := ⋯, ordered := Hex.IsolatedRealRoots.constant._proof_5✝ }

theorem HexRealRootsMathlib.aeval_toPolynomial (p : Hex.ZPoly) (x : ℝ) : (Polynomial.aeval x) (HexPolyZMathlib.toPolynomial p) = ∑ i ∈ Finset.range (Hex.DensePoly.size p), ↑(Hex.DensePoly.coeff p i) * x ^ i

aeval over ℝ of an embedded integer polynomial is the degree-indexed sum of its integer coefficients cast to ℝ — the coefficient-sum form of eval_toPolyℝ, reconciled through the existing aeval_eq_eval_toPolyℝ. For a literal ofCoeffs this unfolds via Finset.sum_range_succ into an explicit polynomial in x.

theorem HexRealRootsMathlib.aeval_toPolynomial_ofCoeffs (coeffs : Array ℤ) (x : ℝ) : (Polynomial.aeval x) (HexPolyZMathlib.toPolynomial (Hex.DensePoly.ofCoeffs coeffs)) = ∑ i ∈ Finset.range coeffs.size, ↑((Hex.DensePoly.ofCoeffs coeffs).coeff i) * x ^ i

The aeval-of-ofCoeffs bridge summed over the raw coefficient array length rather than the trimmed size: extending the sum only adds the trailing zeros. Because coeffs.size for a literal #[…] reduces to a numeral, this is the shape the isolate_roots_bridge tactic unrolls with Finset.sum_range_succ without a decide on the trimmed size.

theorem HexRealRootsMathlib.isRoot_toPolyℝ_iff (p : Hex.ZPoly) (x : ℝ) : (toPolyℝ p).IsRoot x ↔ (Polynomial.aeval x) (HexPolyZMathlib.toPolynomial p) = 0

IsRoot of the real cast is the structure's aeval = 0 form.

theorem HexRealRootsMathlib.ne_zero_of_size_ne_zero {p : Hex.ZPoly} (h : Hex.DensePoly.size p ≠ 0) : p ≠ 0

A ZPoly with nonzero stored size is nonzero. Emitted p ≠ 0 proofs go through this (a Nat decide on p.size), never through structural DensePoly equality (the core Array.instDecidableEqImpl module bug).

noncomputable def Hex.IsolatedRealRoots.of (p : ZPoly) (hp0 : p ≠ 0) (hsf : p.SquareFreeRat) (out : RealRootIsolations p) : IsolatedRealRoots (HexPolyZMathlib.toPolynomial p) out.isolations.size

IsolatedRealRoots.of. Assemble the user structure from a complete Sturm-certified run, via exists_unique_root + isolates + the aeval bridge, including the ordered field from the backend's ordered.

Equations

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

theorem HexRealRootsMathlib.RealRootIsolation.count_one_of_cert {p : Hex.ZPoly} {chain : Array Hex.ZPoly} (hcert : Hex.SturmChainCert p chain) (I : Hex.DyadicInterval) (h : ↑(Hex.sturmVarAt chain I.lower) - ↑(Hex.sturmVarAt chain I.upper) = 1) : p.sturmCount I = 1

A per-interval count_one witness from the chain certificate and a single sign-variation gap decide: sturmCount_eq_of_cert rewrites the certified count onto the literal chain, where the emitted decide confirms the gap is 1.

noncomputable def Hex.IsolatedRealRoots.ofCert {p : ZPoly} {chain : Array ZPoly} {n : ℕ} (iso : Vector (RealRootIsolation p) n) (hsize : DensePoly.size p ≠ 0) (hsf : p.hasSquarefreeSturmChain = true) (hcert : SturmChainCert p chain) (hordered : orderedAdjacent iso.toArray = true) (hcomplete : sturmVarNegInf chain - sturmVarPosInf chain = n) : IsolatedRealRoots (HexPolyZMathlib.toPolynomial p) n

The replay constructor IsolatedRealRoots.ofCert. The production certificate shape: from the reified polynomial p, a reified Sturm chain chain, and n certified isolations iso (each carrying its interval and a cheap count_one_of_cert witness), assemble the isolation with every remaining obligation a single decide on literals:

• hsize : p.size ≠ 0 — nonzeroness by a Nat decide;

• hsf : hasSquarefreeSturmChain p — the squarefree side;

• hcert : SturmChainCert p chain — the reified chain is p's Sturm chain, validated by coefficient-level checks that kernel-reduce (never a structural Array equality), used for complete;

• hordered : orderedAdjacent iso.toArray — the O(n) adjacent-pair order check, walked to the all-pairs ordered field by ordered_of_adjacent;

• hcomplete : sturmVarNegInf chain − sturmVarPosInf chain = n — the −∞/+∞ sign-variation gap, giving complete via rootCount_eq_of_cert.

The kernel replays only the exposed count-check closure against the literal chain; it never rebuilds sturmChain p inside a field.

Equations

• Hex.IsolatedRealRoots.ofCert iso hsize hsf hcert hordered hcomplete = ⋯ ▸ Hex.IsolatedRealRoots.of p ⋯ ⋯ { isolations := iso.toArray, ordered := ⋯, complete := ⋯ }

noncomputable def Hex.IsolatedRealRoots.withIntervals {R : Type u_1} [CommRing R] [Algebra R ℝ] {P : Polynomial R} {n : ℕ} (H : IsolatedRealRoots P n) (w : Vector (ℚ × ℚ) n) (hw : ∀ (i : Fin n), ↑w[i].1 = ↑H.intervals[i].1 ∧ ↑w[i].2 = ↑H.intervals[i].2) : IsolatedRealRoots P n

Re-express an isolation over different interval literals: any vector whose endpoints agree with the originals as reals carries the same three theorems. Stating the agreement over ℝ matters: it never normalizes a rational (no Rat gcd anywhere near the kernel), so the elaborator can discharge it by norm_num through the dyadic cast lemmas and present the intervals as pretty m / 2^k literals. With a literal intervals field, user-side extraction is a definitional step: show H.intervals = #v[…] from rfl.

Equations

• H.withIntervals w hw = { intervals := w, unique_root := ⋯, covers := ⋯, ordered := ⋯ }

@[simp]

theorem Hex.IsolatedRealRoots.withIntervals_intervals {R : Type u_1} [CommRing R] [Algebra R ℝ] {P : Polynomial R} {n : ℕ} (H : IsolatedRealRoots P n) (w : Vector (ℚ × ℚ) n) (hw : ∀ (i : Fin n), ↑w[i].1 = ↑H.intervals[i].1 ∧ ↑w[i].2 = ↑H.intervals[i].2) : (H.withIntervals w hw).intervals = w

withIntervals sets the intervals to the supplied literal vector, so simp reduces a re-based isolation's intervals to that literal.

theorem Hex.IsolatedRealRoots.ofCert_intervals {p : ZPoly} {chain : Array ZPoly} {n : ℕ} (iso : Vector (RealRootIsolation p) n) (hsize : DensePoly.size p ≠ 0) (hsf : p.hasSquarefreeSturmChain = true) (hcert : SturmChainCert p chain) (hordered : orderedAdjacent iso.toArray = true) (hcomplete : sturmVarNegInf chain - sturmVarPosInf chain = n) (i : Fin n) : (ofCert iso hsize hsf hcert hordered hcomplete).intervals[i] = (iso[i].interval.lower.toRat, iso[i].interval.upper.toRat)

The intervals of ofCert are the toRat images of the supplied isolations' dyadic endpoints.

noncomputable def Hex.IsolatedRealRoots.ofCertPretty {p : ZPoly} {chain : Array ZPoly} {n : ℕ} (iso : Vector (RealRootIsolation p) n) (w : Vector (ℚ × ℚ) n) (hsize : DensePoly.size p ≠ 0) (hsf : p.hasSquarefreeSturmChain = true) (hcert : SturmChainCert p chain) (hordered : orderedAdjacent iso.toArray = true) (hcomplete : sturmVarNegInf chain - sturmVarPosInf chain = n) (hw : ∀ (i : Fin n), ↑w[i].1 = HexRealRootsMathlib.Dyadic.toReal iso[i].interval.lower ∧ ↑w[i].2 = HexRealRootsMathlib.Dyadic.toReal iso[i].interval.upper) : IsolatedRealRoots (HexPolyZMathlib.toPolynomial p) n

ofCert, re-based on pretty rational interval literals. w's endpoints are tied to the isolations' dyadics by ℝ-level identities against the literal iso argument — a shape user modules can check without reducing any of this library's definitions, and with no Rat normalization near the kernel. This is the constructor the isolate_roots elaborator emits: with intervals definitionally the literal w, user-side extraction is show H.intervals = #v[…] from rfl.

Equations

• Hex.IsolatedRealRoots.ofCertPretty iso w hsize hsf hcert hordered hcomplete hw = (Hex.IsolatedRealRoots.ofCert iso hsize hsf hcert hordered hcomplete).withIntervals w ⋯

@[simp]

theorem Hex.IsolatedRealRoots.ofCertPretty_intervals {p : ZPoly} {chain : Array ZPoly} {n : ℕ} (iso : Vector (RealRootIsolation p) n) (w : Vector (ℚ × ℚ) n) (hsize : DensePoly.size p ≠ 0) (hsf : p.hasSquarefreeSturmChain = true) (hcert : SturmChainCert p chain) (hordered : orderedAdjacent iso.toArray = true) (hcomplete : sturmVarNegInf chain - sturmVarPosInf chain = n) (hw : ∀ (i : Fin n), ↑w[i].1 = HexRealRootsMathlib.Dyadic.toReal iso[i].interval.lower ∧ ↑w[i].2 = HexRealRootsMathlib.Dyadic.toReal iso[i].interval.upper) : (ofCertPretty iso w hsize hsf hcert hordered hcomplete hw).intervals = w

ofCertPretty's intervals are the supplied literal vector w. The elaborator emits ofCertPretty directly, so this simp lemma lets a user simp/simpa/grind compute an isolation's intervals to their literal endpoints without unfolding the constructor by hand.

def HexRealRootsMathlib.isolateRootsBridge : Lean.ParserDescr

Close ∀ x : ℝ, aeval x (toPolynomial (ofCoeffs #[…])) = 0 ↔ aeval x P = 0 for a reflected literal ofCoeffs polynomial and a user polynomial P over X, C, numerals, +, -, *, ^, neg. The left side unfolds through aeval_toPolynomial_ofCoeffs (a sum over the raw coefficient-array length, whose size reduces to a numeral) and Finset.sum_range_succ; the right side unfolds through the pointwise aeval homomorphism lemmas; push_cast/norm_num/ring_nf reconcile the two explicit polynomials in x.

This is a pointwise evaluation bridge, not a Polynomial identity: it works on closed literal data with integer coefficients and does not attempt to match Polynomial structure.

Equations

• HexRealRootsMathlib.isolateRootsBridge = Lean.ParserDescr.node `HexRealRootsMathlib.isolateRootsBridge 1024 (Lean.ParserDescr.nonReservedSymbol "isolate_roots_bridge" false)