noncomputable def HexRealRootsMathlib.mobiusPoly {R : Type u_1} [CommRing R] (n : ℕ) (a b : R) (P : Polynomial R) : Polynomial R

The abstract Möbius transform over a commutative ring: clears to the (a, b) window, homogenizes at degree n, and shifts back to the positive axis. Built from Mathlib primitives so reflect_mul and the composition lemmas apply directly.

Equations

• HexRealRootsMathlib.mobiusPoly n a b P = (Polynomial.reflect n ((P.comp (Polynomial.X + Polynomial.C b)).comp (Polynomial.C (a - b) * Polynomial.X))).comp (Polynomial.X + Polynomial.C 1)

noncomputable def HexRealRootsMathlib.mobiusInner {R : Type u_1} [CommRing R] (a b : R) (P : Polynomial R) : Polynomial R

The inner (pre-reflection) polynomial of the Möbius transform.

Equations

• HexRealRootsMathlib.mobiusInner a b P = (P.comp (Polynomial.X + Polynomial.C b)).comp (Polynomial.C (a - b) * Polynomial.X)

theorem HexRealRootsMathlib.mobiusPoly_eq_reflect_comp {R : Type u_1} [CommRing R] (n : ℕ) (a b : R) (P : Polynomial R) : mobiusPoly n a b P = (Polynomial.reflect n (mobiusInner a b P)).comp (Polynomial.X + Polynomial.C 1)

theorem HexRealRootsMathlib.mobiusPoly_map {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (φ : R →+* S) (n : ℕ) (a b : R) (P : Polynomial R) : Polynomial.map φ (mobiusPoly n a b P) = mobiusPoly n (φ a) (φ b) (Polynomial.map φ P)

Ring-hom commutation. The Möbius transform commutes with mapping along a ring homomorphism φ: every stage (X + C shift, C (a-b) * X dilation, reflect, the final X + C 1 shift) is built from comp, reflect, C, X, +, *, -, which all commute with Polynomial.map φ. This is the bridge from the real transform to its complex-root picture (φ = algebraMap ℝ ℂ).

theorem HexRealRootsMathlib.natDegree_mobiusInner_le {R : Type u_1} [CommRing R] (a b : R) (P : Polynomial R) : (mobiusInner a b P).natDegree ≤ P.natDegree

The inner Möbius polynomial has degree at most that of P: composing with the degree-one shift X + C b preserves degree, and composing with the (at most) degree-one dilation C (a-b) * X cannot raise it. Proved without Nontrivial R (both linear factors are bounded by degree 1).

theorem HexRealRootsMathlib.natDegree_reflect_le {R : Type u_1} [CommRing R] {N : ℕ} {f : Polynomial R} (hf : f.natDegree ≤ N) : (Polynomial.reflect N f).natDegree ≤ N

natDegree (reflect N f) ≤ N when f.natDegree ≤ N: reflection sends the support into [0, N].

theorem HexRealRootsMathlib.eval_reflect {K : Type u_1} [Field K] {N : ℕ} {f : Polynomial K} (hf : f.natDegree ≤ N) {z : K} (hz : z ≠ 0) : Polynomial.eval z (Polynomial.reflect N f) = z ^ N * Polynomial.eval z⁻¹ f

Reflect evaluation. Over a field, for f.natDegree ≤ N and z ≠ 0, (reflect N f).eval z = z^N * f.eval z⁻¹: reflection is the x ↦ 1/x homogenization at degree N.

theorem HexRealRootsMathlib.mobiusPoly_mul {R : Type u_1} [CommRing R] {n₁ n₂ : ℕ} (a b : R) {P Q : Polynomial R} (hP : P.natDegree ≤ n₁) (hQ : Q.natDegree ≤ n₂) : mobiusPoly (n₁ + n₂) a b (P * Q) = mobiusPoly n₁ a b P * mobiusPoly n₂ a b Q

Multiplicativity of the Möbius transform. With degrees split across the two factors, mobiusPoly of a product is the product of the transforms. The degree hypotheses feed reflect_mul.

theorem HexRealRootsMathlib.mobiusPoly_eval {K : Type u_1} [Field K] {n : ℕ} (a b : K) {P : Polynomial K} (hP : P.natDegree ≤ n) {z : K} (hz : 1 + z ≠ 0) : Polynomial.eval z (mobiusPoly n a b P) = (1 + z) ^ n * Polynomial.eval ((a + b * z) / (1 + z)) P

Evaluation identity. Over a field, for P.natDegree ≤ n and 1 + z ≠ 0, (mobiusPoly n a b P).eval z = (1+z)^n * P.eval ((a+b*z)/(1+z)). This is the Möbius map t ↦ (a + b t)/(1 + t) cleared to a polynomial: positive real roots t of mobiusPoly correspond to real roots of P at (a + b t)/(1 + t).

theorem HexRealRootsMathlib.mobiusPoly_eval_neg_one {R : Type u_1} [CommRing R] (n : ℕ) (a b : R) (P : Polynomial R) : Polynomial.eval (-1) (mobiusPoly n a b P) = (P.comp (Polynomial.X + Polynomial.C b)).coeff n * (a - b) ^ n

Value at -1. (mobiusPoly n a b P).eval (-1) = (P.comp (X + C b)).coeff n · (a-b)^n. The homogenization sends the top coefficient to the constant term, read off at -1 (which the final X + 1 shift sends to 0).

theorem HexRealRootsMathlib.coeff_comp_X_add_C_natDegree {K : Type u_1} [Field K] (P : Polynomial K) (b : K) : (P.comp (Polynomial.X + Polynomial.C b)).coeff P.natDegree = P.leadingCoeff

Shifting by X + C b preserves the top coefficient: at the natural degree, (P.comp (X + C b)).coeff = P.leadingCoeff.

theorem HexRealRootsMathlib.mobiusPoly_eval_neg_one_leading {K : Type u_1} [Field K] {n : ℕ} (a b : K) {P : Polynomial K} (hn : P.natDegree = n) : Polynomial.eval (-1) (mobiusPoly n a b P) = P.leadingCoeff * (a - b) ^ n

Value at -1, leading form. When n = natDegree P, the value at -1 is P.leadingCoeff · (a-b)^n.

theorem HexRealRootsMathlib.mobiusPoly_ne_zero {K : Type u_1} [Field K] {n : ℕ} (a b : K) {P : Polynomial K} (hab : a ≠ b) (hP : P ≠ 0) (hn : P.natDegree = n) : mobiusPoly n a b P ≠ 0

Nonvanishing. For a ≠ b and P ≠ 0 at its own degree, the transform is nonzero: its value at -1 is P.leadingCoeff · (a-b)^n ≠ 0.

theorem HexRealRootsMathlib.mobiusPoly_X_sub_C {K : Type u_1} [Field K] (a b w : K) (hwb : w ≠ b) : mobiusPoly 1 a b (Polynomial.X - Polynomial.C w) = Polynomial.C (b - w) * (Polynomial.X - Polynomial.C ((w - a) / (b - w)))

Linear value (interior). For w ≠ b, the degree-one transform maps the factor X - C w to C (b-w) · (X - C ((w-a)/(b-w))): the root w of X - C w goes to (w-a)/(b-w).

theorem HexRealRootsMathlib.mobiusPoly_X_sub_C_upper {R : Type u_1} [CommRing R] (a b : R) : mobiusPoly 1 a b (Polynomial.X - Polynomial.C b) = Polynomial.C (a - b)

Linear value (right endpoint). The factor X - C b (a root at the excluded upper endpoint) collapses to the constant C (a - b): it has no positive-root image.

theorem HexRealRootsMathlib.mobiusPoly_C {R : Type u_1} [CommRing R] (a b c : R) : mobiusPoly 0 a b (Polynomial.C c) = Polynomial.C c

mobiusPoly 0 fixes constants.

theorem HexRealRootsMathlib.mobiusPoly_one {R : Type u_1} [CommRing R] (a b : R) : mobiusPoly 0 a b 1 = 1

mobiusPoly 0 fixes 1.

theorem HexRealRootsMathlib.mobiusPoly_pow {R : Type u_1} [CommRing R] {k : ℕ} (a b : R) {Q : Polynomial R} (hQ : Q.natDegree ≤ k) (m : ℕ) : mobiusPoly (m * k) a b (Q ^ m) = mobiusPoly k a b Q ^ m

Power form of multiplicativity: with a degree bound per factor, mobiusPoly of a power is the power of the transform.

theorem HexRealRootsMathlib.mobiusPoly_ne_zero_of_ne {K : Type u_1} [Field K] {k : ℕ} {a b : K} (hab : a ≠ b) {P : Polynomial K} (hP : P ≠ 0) : mobiusPoly k a b P ≠ 0

Nonvanishing, degree-free form. Over a field, for a ≠ b, the Möbius transform of a nonzero polynomial is nonzero at every window degree k: each pipeline stage (X + C shifts, the C (a-b) * X dilation, reflect) reflects zeroness.

theorem HexRealRootsMathlib.rootMultiplicity_mobiusPoly {K : Type u_1} [Field K] {n : ℕ} {a b w : K} (hab : a ≠ b) (hwb : w ≠ b) {P : Polynomial K} (hP : P ≠ 0) (hdeg : P.natDegree ≤ n) : Polynomial.rootMultiplicity ((w - a) / (b - w)) (mobiusPoly n a b P) = Polynomial.rootMultiplicity w P

Root-multiplicity correspondence. Over a field, for a ≠ b and a target w ≠ b, the multiplicity of (w-a)/(b-w) in the transform equals the multiplicity of w in P.

theorem HexRealRootsMathlib.pos_root_mobiusPoly_iff {n : ℕ} {a b : ℝ} (hab : a < b) {P : Polynomial ℝ} (hdeg : P.natDegree ≤ n) {t : ℝ} : 0 < t ∧ (mobiusPoly n a b P).IsRoot t ↔ ∃ w ∈ Set.Ioo a b, P.IsRoot w ∧ t = (w - a) / (b - w)

Positive-root correspondence over ℝ. For a < b and natDegree P ≤ n, the positive roots of the transform are exactly the images of the roots of P in the open interval (a, b) under w ↦ (w-a)/(b-w).

theorem HexRealRootsMathlib.countP_roots_mobiusPoly {n : ℕ} {a b : ℝ} (hab : a < b) {P : Polynomial ℝ} (hP : P ≠ 0) (hdeg : P.natDegree ≤ n) : Multiset.countP (fun (t : ℝ) => 0 < t) (mobiusPoly n a b P).roots = Multiset.countP (fun (w : ℝ) => a < w ∧ w < b) P.roots

Windowed root-count correspondence over ℝ. For a < b, P ≠ 0, and natDegree P ≤ n, the number of positive roots of the transform (with multiplicity) equals the number of roots of P in the open interval (a, b).

theorem HexRealRootsMathlib.roots_mobiusPoly {a b : ℂ} (hab : a ≠ b) {P : Polynomial ℂ} (hP : P ≠ 0) : (mobiusPoly P.natDegree a b P).roots = Multiset.map (fun (w : ℂ) => (w - a) / (b - w)) (Multiset.filter (fun (x : ℂ) => x ≠ b) P.roots)

Complex root image. Over ℂ, for a ≠ b and P ≠ 0, the roots of the Möbius transform at the exact degree n = natDegree P are the images of the roots of P other than b under w ↦ (w-a)/(b-w): the b-roots escape to infinity via the degree drop in the homogenization.

theorem HexRealRootsMathlib.signVariations_reverse (l : List ℝ) : Sturm.signVariations l.reverse = Sturm.signVariations l

Sturm.signVariations is invariant under reversal (reading the coefficient list forwards or backwards gives the same count).

theorem HexRealRootsMathlib.sturm_signVariations_range_eq (P : Polynomial ℝ) : Sturm.signVariations (List.map P.coeff (List.range (P.natDegree + 1))) = P.signVariations

Descending-list variation bridge. For any real polynomial, the abstract Sturm.signVariations of the ascending coefficient list equals Mathlib's Polynomial.signVariations (which reads the descending coeffList).

theorem HexRealRootsMathlib.descartesVar_eq_signVariations (q : Hex.ZPoly) : Hex.descartesVar q = (toPolyℝ q).signVariations

Descartes variation bridge. The executable Hex.descartesVar q equals Mathlib's Polynomial.signVariations (toPolyℝ q). The executable count is on the ascending sign list; the abstract count on the descending coeffList; the two agree by reversal invariance and the destutter identity above.

def HexRealRootsMathlib.numExp : Dyadic → ℤ × ℤ

Public mirror of the private Hex.dyadicNumExp: the (numerator, denominator-exponent) pair of a dyadic value.

Equations

• HexRealRootsMathlib.numExp Dyadic.zero = (0, 0)
• HexRealRootsMathlib.numExp (Dyadic.ofOdd n k hn) = (n, k)

def HexRealRootsMathlib.endpoints (I : Hex.DyadicInterval) : ℤ × ℤ × ℕ

Public mirror of the private Hex.mobiusEndpoints: the integer endpoint numerators over the common power-of-two denominator 2^s.

Equations

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

noncomputable def HexRealRootsMathlib.mobiusSteps (p : Hex.ZPoly) (α β : ℤ) (s : ℕ) : Hex.ZPoly

Public mirror of the Hex.mobiusTransform pipeline past the endpoint computation, parameterized by the integer data (α, β, s).

Equations

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

theorem HexRealRootsMathlib.mobiusTransform_eq_steps (p : Hex.ZPoly) (I : Hex.DyadicInterval) : Hex.mobiusTransform p I = mobiusSteps p (endpoints I).1 (endpoints I).2.1 (endpoints I).2.2

The executable transform is the mirrored pipeline at the mirrored endpoint data: both sides reduce to the same term once the endpoint constructors are split.

theorem HexRealRootsMathlib.toPolyℝ_compose (p q : Hex.ZPoly) : toPolyℝ (Hex.DensePoly.compose p q) = (toPolyℝ p).comp (toPolyℝ q)

The real cast intertwines the executable Horner composition with Polynomial.comp.

theorem HexRealRootsMathlib.toPolyℝ_dilate (c : ℤ) (q : Hex.ZPoly) : toPolyℝ (Hex.ZPoly.dilate c q) = (toPolyℝ q).comp (Polynomial.C ↑c * Polynomial.X)

The real cast turns the executable dilation into composition with C c * X.

theorem HexRealRootsMathlib.toPolyℝ_mobiusTransform (p : Hex.ZPoly) (I : Hex.DyadicInterval) (hdeg : 1 ≤ Hex.DensePoly.natDegree p) : toPolyℝ (Hex.mobiusTransform p I) = Polynomial.C (2 ^ ((endpoints I).2.2 * Hex.DensePoly.natDegree p)) * mobiusPoly (Hex.DensePoly.natDegree p) (Dyadic.toReal I.lower) (Dyadic.toReal I.upper) (toPolyℝ p)

The executable Möbius bridge. For positive-degree p, the real cast of Hex.mobiusTransform p I is 2^{s·n} times the abstract mobiusPoly at the real endpoint values, with n the degree of p and s the common denominator exponent of I's endpoints.

theorem HexRealRootsMathlib.toPolyℝ_mobiusTransform' (p : Hex.ZPoly) (I : Hex.DyadicInterval) (hdeg : 1 ≤ Hex.DensePoly.natDegree p) : ∃ (c : ℝ), 0 < c ∧ toPolyℝ (Hex.mobiusTransform p I) = Polynomial.C c * mobiusPoly (Hex.DensePoly.natDegree p) (Dyadic.toReal I.lower) (Dyadic.toReal I.upper) (toPolyℝ p)

Positivity of the clearing factor: existential form of the bridge for consumers that only need toPolyℝ (mobiusTransform p I) to be a positive constant multiple of the abstract transform.

theorem HexRealRootsMathlib.descartesVar_mobiusTransform (p : Hex.ZPoly) (I : Hex.DyadicInterval) (hdeg : 1 ≤ Hex.DensePoly.natDegree p) : Hex.descartesVar (Hex.mobiusTransform p I) = (mobiusPoly (Hex.DensePoly.natDegree p) (Dyadic.toReal I.lower) (Dyadic.toReal I.upper) (toPolyℝ p)).signVariations

The Descartes count of the transform is the abstract sign-variation count. The 2^{s·n} clearing factor is absorbed by Polynomial.signVariations_C_mul; this is the form the engine proof cites.