@[reducible, inline]

noncomputable abbrev HexRealRootsMathlib.toPolyℚ (p : Hex.ZPoly) : Polynomial ℚ

Compatibility alias for the rational cast, now shared by integer-polynomial companions.

Equations

• HexRealRootsMathlib.toPolyℚ p = HexPolyZMathlib.toPolyℚ p

theorem HexRealRootsMathlib.size_le_one_iff_natDegree_eq_zero {R : Type u_1} [Semiring R] [DecidableEq R] (g : Hex.DensePoly R) : g.size ≤ 1 ↔ (HexPolyMathlib.toPolynomial g).natDegree = 0

theorem HexRealRootsMathlib.toPolynomial_toRatPoly (f : Hex.ZPoly) : HexPolyMathlib.toPolynomial f.toRatPoly = toPolyℚ f

theorem HexRealRootsMathlib.coeff_toPolyℚ (p : Hex.ZPoly) (n : ℕ) : (toPolyℚ p).coeff n = ↑(Hex.DensePoly.coeff p n)

theorem HexRealRootsMathlib.eval_toPolyℚ (p : Hex.ZPoly) (x : ℚ) : Polynomial.eval x (toPolyℚ p) = ∑ i ∈ Finset.range (Hex.DensePoly.size p), ↑(Hex.DensePoly.coeff p i) * x ^ i

theorem HexRealRootsMathlib.toPolyℚ_ne_zero {f : Hex.ZPoly} (hf : f ≠ 0) : toPolyℚ f ≠ 0

theorem HexRealRootsMathlib.squareFreeRat_iff (f : Hex.ZPoly) (hf : f ≠ 0) : f.SquareFreeRat ↔ Squarefree (toPolyℚ f)

Compatibility alias for the shared rational squarefreeness bridge.

theorem HexRealRootsMathlib.toReal_add (a b : Dyadic) : Dyadic.toReal (a + b) = Dyadic.toReal a + Dyadic.toReal b

Dyadic.toReal is additive.

theorem HexRealRootsMathlib.toReal_mul (a b : Dyadic) : Dyadic.toReal (a * b) = Dyadic.toReal a * Dyadic.toReal b

Dyadic.toReal is multiplicative.

@[simp]

theorem HexRealRootsMathlib.toReal_zero : Dyadic.toReal 0 = 0

Dyadic.toReal sends 0 to 0.

theorem HexRealRootsMathlib.toReal_evalDyadic (q : Hex.ZPoly) (x : Dyadic) : Dyadic.toReal (q.evalDyadic x) = Polynomial.eval (Dyadic.toReal x) (toPolyℝ q)

Evaluation correspondence. The exact dyadic Horner evaluation of an integer polynomial, cast to ℝ, agrees with the Mathlib evaluation of its real cast at the real value of the dyadic point.

theorem HexRealRootsMathlib.sign_dyadicSign (d : Dyadic) : SignType.sign ↑(Hex.dyadicSign d) = SignType.sign (Dyadic.toReal d)

Sign correspondence. The exact integer sign of a dyadic value has, as a real number, the same SignType.sign as the real value of the dyadic.

theorem HexRealRootsMathlib.evalSign_zero_iff (p : Hex.ZPoly) (x : Dyadic) : Hex.dyadicSign (p.evalDyadic x) = 0 ↔ (toPolyℝ p).IsRoot (Dyadic.toReal x)

Exact dyadic Horner evaluation has zero sign exactly at a real root.

theorem HexRealRootsMathlib.signVar_eq (l : List ℤ) : Hex.signVar l = Sturm.signVariations (List.map Int.cast l)

Sign-variation count correspondence. The executable integer sign-variation count of a list equals the abstract real sign-variation count of the list cast to ℝ.

theorem HexRealRootsMathlib.sturmVarAt_eq (chain : Array Hex.ZPoly) (x : Dyadic) : Hex.sturmVarAt chain x = Sturm.sturmVar (List.map toPolyℝ chain.toList) (Dyadic.toReal x)

Sign-variation correspondence. The executable Sturm sign-variation count of a chain at a dyadic point equals the abstract Sturm.sturmVar of the mapped real chain at the real value of the point. Positive scaling of chain elements is irrelevant: sturmVar reads only signs, which the exact dyadic evaluation and the Mathlib evaluation agree on.

theorem HexRealRootsMathlib.toPolynomial_scale {R : Type u_1} [CommRing R] [DecidableEq R] (c : R) (p : Hex.DensePoly R) : HexPolyMathlib.toPolynomial (Hex.DensePoly.scale c p) = Polynomial.C c * HexPolyMathlib.toPolynomial p

toPolynomial turns the executable scalar multiply into C-multiplication.

theorem HexRealRootsMathlib.toPolynomial_shift {R : Type u_1} [CommRing R] [DecidableEq R] (k : ℕ) (p : Hex.DensePoly R) : HexPolyMathlib.toPolynomial (Hex.DensePoly.shift k p) = Polynomial.X ^ k * HexPolyMathlib.toPolynomial p

toPolynomial turns the executable x^k shift into X^k-multiplication.

theorem HexRealRootsMathlib.toPolyℝ_scale (c : ℤ) (p : Hex.ZPoly) : toPolyℝ (Hex.DensePoly.scale c p) = Polynomial.C ↑c * toPolyℝ p

The real cast of a scalar multiple.

theorem HexRealRootsMathlib.toPolyℝ_add (p q : Hex.ZPoly) : toPolyℝ (p + q) = toPolyℝ p + toPolyℝ q

The real cast is additive.

theorem HexRealRootsMathlib.toPolyℝ_shift (k : ℕ) (p : Hex.ZPoly) : toPolyℝ (Hex.DensePoly.shift k p) = Polynomial.X ^ k * toPolyℝ p

The real cast of an x^k shift.

theorem HexRealRootsMathlib.toPolyℝ_sub (p q : Hex.ZPoly) : toPolyℝ (p - q) = toPolyℝ p - toPolyℝ q

The real cast of a difference.

theorem HexRealRootsMathlib.leadingCoeff_toPolyℝ (p : Hex.ZPoly) : (toPolyℝ p).leadingCoeff = ↑(Hex.DensePoly.leadingCoeff p)

The real cast preserves the leading coefficient.

theorem HexRealRootsMathlib.toPolyℝ_spem (f g : Hex.ZPoly) (hg : Hex.DensePoly.leadingCoeff g ≠ 0) (hdeg : 1 ≤ Hex.DensePoly.natDegree g) : ∃ (c : ℝ) (Q : Polynomial ℝ), 0 < c ∧ Polynomial.C c * toPolyℝ f = Q * toPolyℝ g + toPolyℝ (f.spem g)

The spem correspondence. For a nonconstant divisor g (positive degree, hence nonzero leading coefficient), the executable sign-managed pseudo-remainder spem f g is a positive real multiple of the field remainder of f by g: there is c > 0 and a quotient Q with C c · toPolyℝ f = Q · toPolyℝ g + toPolyℝ (spem f g). Evaluating at a zero x of g collapses this to c · f(x) = (spem f g)(x), the sign-transfer identity the chain axioms consume.

theorem HexRealRootsMathlib.toPolyℝ_neg (p : Hex.ZPoly) : toPolyℝ (-p) = -toPolyℝ p

The real cast of a negation.

theorem HexRealRootsMathlib.toPolyℝ_mul (p q : Hex.ZPoly) : toPolyℝ (p * q) = toPolyℝ p * toPolyℝ q

The real cast is multiplicative.

@[simp]

theorem HexRealRootsMathlib.toPolyℝ_zero : toPolyℝ 0 = 0

The real cast of the zero polynomial.

theorem HexRealRootsMathlib.toPolyℝ_eq_zero_iff {p : Hex.ZPoly} : toPolyℝ p = 0 ↔ p = 0

The real cast is zero exactly when the executable polynomial is.

theorem HexRealRootsMathlib.content_real_pos {p : Hex.ZPoly} (hp : p ≠ 0) : 0 < ↑p.content

The real value of the content of a nonzero polynomial is positive: the executable content is a nonnegative integer, nonzero for nonzero input.

theorem HexRealRootsMathlib.toPolyℝ_eq_C_content_mul_primitivePart (p : Hex.ZPoly) : toPolyℝ p = Polynomial.C ↑p.content * toPolyℝ p.primitivePart

Gauss decomposition of the real cast: a polynomial is its (positive integer) content times its primitive part.

theorem HexRealRootsMathlib.primitivePart_ne_zero {p : Hex.ZPoly} (hp : p ≠ 0) : p.primitivePart ≠ 0

The primitive part of a nonzero polynomial is nonzero.

theorem HexRealRootsMathlib.toPolyℝ_derivative (p : Hex.ZPoly) : toPolyℝ (Hex.DensePoly.derivative p) = Polynomial.derivative (toPolyℝ p)

The real cast commutes with the derivative.

theorem HexRealRootsMathlib.separable_toPolyℝ (p : Hex.ZPoly) (hsq : Squarefree (toPolyℚ p)) : (toPolyℝ p).Separable

Squarefree-to-separable transfer. If the rational cast toPolyℚ p is squarefree, its real cast toPolyℝ p is separable. Over the perfect field ℚ, squarefree means separable, and separability is preserved by the field extension ℚ → ℝ.

theorem HexRealRootsMathlib.roots_toPolyℝ_eq_primitivePart (p : Hex.ZPoly) (hp : p ≠ 0) : (toPolyℝ p).roots = (toPolyℝ p.primitivePart).roots

The real cast of a nonzero p is the positive-content multiple of the cast of its primitive part, so the two share exactly the same real roots.

theorem HexRealRootsMathlib.sturmChain_map_head? (p : Hex.ZPoly) (hp : 1 ≤ Hex.DensePoly.natDegree p) : (List.map toPolyℝ p.sturmChain.toList).head? = some (toPolyℝ p.primitivePart)

Head of the mapped chain. For a positive-degree p, the real-cast Sturm chain has head toPolyℝ (primitivePart p), matching the IsSturmChain.head field (stated at the primitive part, per the design note: the executable chain's first element is primitivePart p, not p, since the content is stripped).

theorem HexRealRootsMathlib.sturmChain_map_ne_nil (p : Hex.ZPoly) (hp : 1 ≤ Hex.DensePoly.natDegree p) : List.map toPolyℝ p.sturmChain.toList ≠ []

Nonemptiness of the mapped chain for a positive-degree p.

theorem HexRealRootsMathlib.coprime_step_rev {p q r : Polynomial ℝ} {a b : ℝ} {d : Polynomial ℝ} (hb : b ≠ 0) (hid : Polynomial.C a * p = d * q - Polynomial.C b * r) (h : IsCoprime q r) : IsCoprime p q

Reverse of coprime_step. The three-term relation C c₀ · a = Q · b − C k · c' (with k ≠ 0) transports IsCoprime b c' back to IsCoprime a b: solving the relation for c' and substituting into a Bezout combination for (b, c') yields one for (a, b).

theorem HexRealRootsMathlib.flank_of_key {s₀ s₁ : Polynomial ℝ} {γ : ℝ} (hγ : 0 < γ) (hkey : Polynomial.derivative s₀ = Polynomial.C γ * s₁) {r : ℝ} (h0 : Polynomial.eval r s₀ = 0) (h1 : Polynomial.eval r s₁ ≠ 0) : (∀ᶠ (x : ℝ) in nhdsWithin r (Set.Iio r), Polynomial.eval x (s₀ * s₁) < 0) ∧ ∀ᶠ (x : ℝ) in nhdsWithin r (Set.Ioi r), 0 < Polynomial.eval x (s₀ * s₁)

The head-pair flank. If s₀ vanishes at r, s₁ does not, and s₀' = C γ · s₁ with γ > 0 (the executable seeds: the primitive parts of p and p'), then s₀ · s₁ is negative just left of r and positive just right: its derivative at r is γ · s₁(r)² > 0.

theorem HexRealRootsMathlib.eval_ne_zero_of_isCoprime {a b : Polynomial ℝ} (h : IsCoprime a b) {x : ℝ} (ha : Polynomial.eval x a = 0) : Polynomial.eval x b ≠ 0

Coprime polynomials never vanish together.

theorem HexRealRootsMathlib.sturmChain_isSturmChain (p : Hex.ZPoly) (hp : 1 ≤ Hex.DensePoly.natDegree p) (hsq : p.SquareFreeRat) : Sturm.IsSturmChain (toPolyℝ p.primitivePart) (List.map toPolyℝ p.sturmChain.toList)

The executable Sturm chain is a Sturm chain. For a positive-degree, rationally squarefree p, the real cast of Hex.ZPoly.sturmChain p satisfies all the Sturm.IsSturmChain sign axioms for toPolyℝ (primitivePart p).

Stated at the primitive part: the executable chain's head is primitivePart p (the content is stripped), so an IsSturmChain (toPolyℝ p) … conclusion would have the wrong head; p and its primitive part have the same real roots (roots_toPolyℝ_eq_primitivePart), so the counting consequences are unaffected.

theorem HexRealRootsMathlib.squareFreeRat_of_hasSquarefreeSturmChain (p : Hex.ZPoly) (h : p.hasSquarefreeSturmChain = true) : p.SquareFreeRat

The Sturm squarefree certificate is sound. If the executable Hex.ZPoly.hasSquarefreeSturmChain p is true — p has positive degree and the terminal element of its Sturm chain is a nonzero constant — then p is squarefree over ℚ. This is the converse packaging of sturmChain_isSturmChain: it lets a concrete SquareFreeRat p be discharged by by decide on the executable chain, sidestepping the non-kernel-reducible rational gcd inside SquareFreeRat itself.

theorem HexRealRootsMathlib.toReal_lt_toReal {a b : Dyadic} (h : a < b) : Dyadic.toReal a < Dyadic.toReal b

Dyadic order transfers to the real values.

theorem HexRealRootsMathlib.toReal_le_toReal {a b : Dyadic} (h : a ≤ b) : Dyadic.toReal a ≤ Dyadic.toReal b

Nonstrict dyadic order transfers to the real values.

theorem HexRealRootsMathlib.toReal_lt_toReal_iff {a b : Dyadic} : Dyadic.toReal a < Dyadic.toReal b ↔ a < b

Dyadic order coincides with the order of the real values.

theorem HexRealRootsMathlib.toReal_midpoint (I : Hex.DyadicInterval) : Dyadic.toReal I.midpoint = (Dyadic.toReal I.lower + Dyadic.toReal I.upper) / 2

The real value of an interval's exact dyadic midpoint.

theorem HexRealRootsMathlib.lower_lt_midpoint (I : Hex.DyadicInterval) : I.lower < I.midpoint

The midpoint is strictly above the lower endpoint.

theorem HexRealRootsMathlib.midpoint_lt_upper (I : Hex.DyadicInterval) : I.midpoint < I.upper

The midpoint is strictly below the upper endpoint.

theorem HexRealRootsMathlib.sturmCount_eq_card_roots (p : Hex.ZPoly) (hp : 1 ≤ Hex.DensePoly.natDegree p) (hsq : p.SquareFreeRat) (I : Hex.DyadicInterval) : p.sturmCount I = ↑(Multiset.filter (fun (r : ℝ) => Dyadic.toReal I.lower < r ∧ r ≤ Dyadic.toReal I.upper) (toPolyℝ p).roots).card

Sturm count correspondence. For positive-degree, rationally squarefree p, the executable Hex.ZPoly.sturmCount p I equals the number of real roots of toPolyℝ p in the half-open interval (I.lower, I.upper].

theorem HexRealRootsMathlib.sturmVarPosInf_eq (chain : Array Hex.ZPoly) : Hex.sturmVarPosInf chain = Sturm.sturmVarPosInf (List.map toPolyℝ chain.toList)

The executable +∞ variation count matches the abstract one: both read the signs of the leading coefficients.

theorem HexRealRootsMathlib.sturmVarNegInf_eq (chain : Array Hex.ZPoly) : Hex.sturmVarNegInf chain = Sturm.sturmVarNegInf (List.map toPolyℝ chain.toList)

The executable −∞ variation count matches the abstract one: both read sign(lc) · (−1)^degree.

theorem HexRealRootsMathlib.rootCount_eq_card_roots (p : Hex.ZPoly) (hp : 1 ≤ Hex.DensePoly.natDegree p) (hsq : p.SquareFreeRat) : p.rootCount = (toPolyℝ p).roots.card

Root count correspondence. For positive-degree, rationally squarefree p, the executable Hex.ZPoly.rootCount p equals the total number of real roots of toPolyℝ p.

theorem HexRealRootsMathlib.sepPrec_separates' (p : Hex.ZPoly) (hp : p ≠ 0) (hsq : p.SquareFreeRat) (z₁ z₂ : ℂ) : (toPolyℂ p).IsRoot z₁ → (toPolyℂ p).IsRoot z₂ → z₁ ≠ z₂ → 2 ^ (-↑(Hex.sepPrec p)) < ‖z₁ - z₂‖ / 4

Separation with the executable squarefreeness test. The public, SquareFreeRat-facing form of sepPrec_separates: for nonzero p passing the executable rational-gcd squarefreeness test, distinct complex roots of toPolyℂ p are more than 4 · 2^{−sepPrec p} apart.