Real-rooted polynomials and interlacing

A real polynomial is real-rooted if it splits over ℝ, i.e. all its complex roots are real. This file develops the predicate, its closure properties, and the sign-change arguments that turn interlacing data into real-rootedness. These are the tools used for the Heilmann–Lieb theorem on matching polynomials and, more generally, by the method of interlacing polynomials of Marcus, Spielman and Srivastava.

Main definitions

• MSS.RealRooted p: p : ℝ[X] splits over ℝ (Polynomial.Splits).
• MSS.BoundedBy p B: p is real-rooted and every root has absolute value at most B.
• MSS.maxRoot p: the largest real root, in WithBot ℝ.
• MSS.Interlaces f g: every member f + t • g of the pencil is real-rooted.
• MSS.Interlace f g: every real combination a • f + b • g is real-rooted.
• MSS.rootsList p: the distinct real roots of p, sorted increasingly.

Main results

• MSS.RealRooted.mul, MSS.RealRooted.prod, MSS.RealRooted.of_dvd: closure properties.
• MSS.realRooted_iff_card_roots: p is real-rooted iff it has natDegree p real roots with multiplicity.
• MSS.card_roots_ge_of_alternating: a polynomial that alternates in sign at n + 1 increasing points has at least n distinct real roots; MSS.realRooted_of_alternating concludes real-rootedness when its degree is at most n.
• MSS.realRooted_comb_of_alternates: if f alternates in sign at n + 1 increasing roots of g, every nonzero combination a • f + b • g with a ≠ 0 and degree at most n is real-rooted.
• MSS.realRooted_of_root_per_gap: a nonzero polynomial of degree at most n with a root in each of the n gaps of an increasing sequence is real-rooted.
• MSS.exists_strictMono_roots: the distinct roots of p ≠ 0 as a strictly increasing family.

References

• A. W. Marcus, D. A. Spielman, N. Srivastava, Interlacing families I: Bipartite Ramanujan graphs of all degrees, Ann. of Math. 182 (2015) 307–325.
• S. Fisk, Polynomials, roots, and interlacing, arXiv:math/0612833.

def MSS.RealRooted (p : Polynomial ℝ) : Prop

A real polynomial is real-rooted if it splits into linear (and constant) factors over ℝ — equivalently, all of its complex roots are real. Defined as the intrinsic Polynomial.Splits, i.e. membership in the multiplicative closure of constants C a and monic linears X + C a.

Equations

• MSS.RealRooted p = p.Splits

theorem MSS.realRooted_zero : RealRooted 0

theorem MSS.realRooted_one : RealRooted 1

theorem MSS.realRooted_C (a : ℝ) : RealRooted (Polynomial.C a)

Constants are real-rooted.

theorem MSS.realRooted_X_sub_C (a : ℝ) : RealRooted (Polynomial.X - Polynomial.C a)

Monic linear factors X - C a are real-rooted.

theorem MSS.RealRooted.mul {p q : Polynomial ℝ} (hp : RealRooted p) (hq : RealRooted q) : RealRooted (p * q)

Real-rootedness is closed under multiplication. Immediate from Splits being membership in a submonoid (Submonoid.mul_mem).

theorem MSS.RealRooted.prod {ι : Type u_1} {s : Finset ι} {f : ι → Polynomial ℝ} (h : ∀ i ∈ s, RealRooted (f i)) : RealRooted (∏ i ∈ s, f i)

Real-rootedness is closed under finite products.

theorem MSS.RealRooted.of_dvd {p q : Polynomial ℝ} (hq : RealRooted q) (hq0 : q ≠ 0) (hpq : p ∣ q) : RealRooted p

A (nonzero) divisor of a real-rooted polynomial is real-rooted. If p ∣ q and q splits over ℝ (with q ≠ 0), the roots of p are a sub-multiset of those of q, hence all real. Thin wrapper around Polynomial.Splits.of_dvd. This is the engine of the connected→real-rooted step (T5): μ(G) ∣ μ(pathTree), and the path tree is a forest.

theorem MSS.realRooted_iff_card_roots {p : Polynomial ℝ} : RealRooted p ↔ p.roots.card = p.natDegree

Root-count characterisation. A real polynomial is real-rooted iff its multiset of (real) roots has cardinality equal to its degree — i.e. it has exactly natDegree real roots counted with multiplicity.

theorem MSS.realRooted_prod_X_sub_C {ι : Type u_1} (s : Finset ι) (a : ι → ℝ) : RealRooted (∏ i ∈ s, (Polynomial.X - Polynomial.C (a i)))

A product of monic linears ∏ (X - C aᵢ) is real-rooted.

def MSS.BoundedBy (p : Polynomial ℝ) (B : ℝ) : Prop

p is bounded by B if it is real-rooted and all of its (real) roots lie in the interval [-B, B]. The Heilmann–Lieb theorem says that the matching polynomial of a graph of maximum degree Δ ≥ 2 is bounded by 2√(Δ-1).

Equations

• MSS.BoundedBy p B = (MSS.RealRooted p ∧ ∀ (x : ℝ), p.IsRoot x → |x| ≤ B)

theorem MSS.BoundedBy.realRooted {p : Polynomial ℝ} {B : ℝ} (h : BoundedBy p B) : RealRooted p

theorem MSS.BoundedBy.of_dvd {p q : Polynomial ℝ} {B : ℝ} (hp : BoundedBy p B) (hp0 : p ≠ 0) (hqp : q ∣ p) : BoundedBy q B

A (nonzero) divisor of a BoundedBy B polynomial is BoundedBy B. Real-rootedness transfers by RealRooted.of_dvd, and every root of the divisor q is a root of p (write p = q * c), so it inherits the |·| ≤ B bound. This is the Heilmann–Lieb transfer step: μ(G) ∣ μ(T(G,u)), and the path tree T(G,u) is a forest whose adjacency eigenvalues lie in [−B, B].

theorem MSS.BoundedBy.prod {ι : Type u_1} {s : Finset ι} {f : ι → Polynomial ℝ} {B : ℝ} (h : ∀ i ∈ s, BoundedBy (f i) B) : BoundedBy (∏ i ∈ s, f i) B

BoundedBy B is closed under finite products. A root of ∏ fᵢ is a root of some factor (ℝ[X] is a domain), hence bounded by B; real-rootedness multiplies (RealRooted.prod).

theorem MSS.boundedBy_prod_X_sub_C {ι : Type u_1} (s : Finset ι) (a : ι → ℝ) {B : ℝ} (hB : ∀ i ∈ s, |a i| ≤ B) : BoundedBy (∏ i ∈ s, (Polynomial.X - Polynomial.C (a i))) B

Fundamental constructor / fusion lemma. A product of linears ∏ (X - C aᵢ) whose roots aᵢ all lie in [-B, B] is BoundedBy B. Both the eigenvalue product (RH side, via IsHermitian.charpoly_eq) and the matching polynomial (MSS side) are of exactly this shape.

Largest real root

noncomputable def MSS.maxRoot (p : Polynomial ℝ) : WithBot ℝ

The largest real root of p, valued in WithBot ℝ so that the empty case (no real roots, e.g. p = 0 or an irreducible-over-ℝ factor) is total: maxRoot p = ⊥. For the method of interlacing polynomials this is the quantity compared across a family — the averaging theorem says some member's maxRoot is at most the maxRoot of the sum.

Equations

• MSS.maxRoot p = p.roots.toFinset.max

@[simp]

theorem MSS.maxRoot_zero : maxRoot 0 = ⊥

theorem MSS.le_maxRoot {p : Polynomial ℝ} {x : ℝ} (hp : p ≠ 0) (hx : p.IsRoot x) : ↑x ≤ maxRoot p

Every real root is ≤ maxRoot.

theorem MSS.maxRoot_le_coe_iff {p : Polynomial ℝ} {B : ℝ} : maxRoot p ≤ ↑B ↔ ∀ x ∈ p.roots, x ≤ B

maxRoot p ≤ B iff every real root is ≤ B.

theorem MSS.BoundedBy.maxRoot_le {p : Polynomial ℝ} {B : ℝ} (h : BoundedBy p B) : maxRoot p ≤ ↑B

A polynomial bounded by B has maxRoot ≤ B: the upper half of the [-B, B] containment, packaged for the interlacing-family argument.

theorem MSS.exists_isRoot_eq_maxRoot {p : Polynomial ℝ} (hp : p ≠ 0) (hr : p.roots ≠ 0) : ∃ (r : ℝ), p.IsRoot r ∧ maxRoot p = ↑r

When p has at least one real root, maxRoot p is attained: it equals ↑r for an actual root r.

def MSS.Interlaces (f g : Polynomial ℝ) : Prop

f and g interlace (pencil form) if every real combination f + t·g of the pencil is real-rooted. This is the operational notion used throughout the method of interlacing polynomials: a common interlacer of a family yields real-rootedness of every convex combination, hence of the average.

Equations

• MSS.Interlaces f g = ∀ (t : ℝ), MSS.RealRooted (f + Polynomial.C t * g)

theorem MSS.Interlaces.realRooted_left {f g : Polynomial ℝ} (h : Interlaces f g) : RealRooted f

An interlacing pencil's left endpoint (t = 0) is real-rooted.

theorem MSS.Interlaces.realRooted_add {f g : Polynomial ℝ} (h : Interlaces f g) : RealRooted (f + g)

If f and g interlace then their sum f + g is real-rooted (the t = 1 point of the pencil). This is the seed of the MSS averaging argument.

The interlacing pencil and its convex cone

def MSS.Interlace (f g : Polynomial ℝ) : Prop

f and g form an interlacing pair if every real linear combination a·f + b·g is real-rooted. By the Hermite–Kakeya–Obreschkoff theorem this is equivalent to f and g having interlacing roots (a common interlacer); we take the algebraic form as the working definition, since MSS proofs manipulate the combinations directly. Strictly stronger than the one-sided pencil Interlaces (take a = 1).

Equations

• MSS.Interlace f g = ∀ (a b : ℝ), MSS.RealRooted (Polynomial.C a * f + Polynomial.C b * g)

theorem MSS.Interlace.realRooted_left {f g : Polynomial ℝ} (h : Interlace f g) : RealRooted f

theorem MSS.Interlace.realRooted_right {f g : Polynomial ℝ} (h : Interlace f g) : RealRooted g

theorem MSS.Interlace.realRooted_add {f g : Polynomial ℝ} (h : Interlace f g) : RealRooted (f + g)

An interlacing pair's sum is real-rooted — the seed of the convex cone.

theorem MSS.Interlace.symm {f g : Polynomial ℝ} (h : Interlace f g) : Interlace g f

theorem MSS.Interlace.comb {f g : Polynomial ℝ} (h : Interlace f g) (a b c d : ℝ) : Interlace (Polynomial.C a * f + Polynomial.C b * g) (Polynomial.C c * f + Polynomial.C d * g)

Convex-cone / pencil structure — the algebraic heart of step 3. If f, g interlace then any two polynomials in their linear pencil span{f, g} interlace each other. Hence the pencil is a 2-dimensional cone all of whose members are mutually real-rooted — the algebraic backbone of the method of interlacing polynomials (every combination encountered in MSS stays real-rooted).

theorem MSS.Interlace.add_interlace_left {f g : Polynomial ℝ} (h : Interlace f g) : Interlace (f + g) f

The pencil is closed under sums (a corollary of comb): f + g interlaces f. This is the cone's additive-closure lemma at the algebraic level.

theorem MSS.Interlace.smul_left {f g : Polynomial ℝ} (h : Interlace f g) (c : ℝ) : Interlace (Polynomial.C c * f) g

Scaling a pencil generator keeps the pair interlacing (cone closed under nonneg — indeed all — real scaling).

HKO bridge — the analytic load-bearing lemmas

theorem MSS.exists_isRoot_of_eval_mul_neg (p : Polynomial ℝ) {x y : ℝ} (hxy : x < y) (h : Polynomial.eval x p * Polynomial.eval y p < 0) : ∃ z ∈ Set.Ioo x y, p.IsRoot z

IVT atom. If a real polynomial takes values of opposite sign at x < y then it has a root strictly between them. This is the intermediate-value theorem specialised to polynomials (continuous), and it is the single analytic primitive out of which the whole Hermite–Kakeya–Obreschkoff sign-change argument is built: each sign alternation of a combination across the roots of its interlacer yields one root via this lemma.

theorem MSS.realRooted_of_natDegree_le_card_roots {p : Polynomial ℝ} (h : p.natDegree ≤ p.roots.card) : RealRooted p

Counting lemma. A polynomial that has at least natDegree real roots (counted with multiplicity) is real-rooted: combined with the always-true reverse bound card_roots' : card ≤ natDegree, exhibiting natDegree real roots forces equality, hence Splits. This is the lemma that converts "the IVT produced enough sign-change roots" into RealRooted.

Ordering the roots (first step of the HKO assembly)

noncomputable def MSS.rootsList (p : Polynomial ℝ) : List ℝ

The sorted list of distinct real roots of p, strictly increasing. This is the combinatorial skeleton on which the HKO sign-change argument runs: the gaps between consecutive entries are where exists_isRoot_of_eval_mul_neg will deposit the roots of a combination.

Equations

• MSS.rootsList p = p.roots.toFinset.sort fun (x1 x2 : ℝ) => x1 ≤ x2

theorem MSS.rootsList_sortedLT (p : Polynomial ℝ) : (rootsList p).SortedLT

The sorted root list is strictly increasing.

theorem MSS.rootsList_nodup (p : Polynomial ℝ) : (rootsList p).Nodup

The sorted root list has no duplicates.

theorem MSS.mem_rootsList {p : Polynomial ℝ} {x : ℝ} : x ∈ rootsList p ↔ x ∈ p.roots

Membership in the sorted root list is membership in the root multiset.

theorem MSS.mem_rootsList_iff_isRoot {p : Polynomial ℝ} (hp : p ≠ 0) {x : ℝ} : x ∈ rootsList p ↔ p.IsRoot x

For p ≠ 0, the sorted root list is exactly the set of real roots.

theorem MSS.length_rootsList (p : Polynomial ℝ) : (rootsList p).length = p.roots.toFinset.card

The length of the sorted root list is the number of distinct real roots.

theorem MSS.isRoot_iff_mem_rootsList {p : Polynomial ℝ} (hp : p ≠ 0) {x : ℝ} : p.IsRoot x ↔ x ∈ rootsList p

Completeness of the ordering. Every real root of p appears in rootsList p; conversely every list entry is a genuine root. Packaged for the gap argument: outside the closed span of rootsList p and between consecutive entries, p has no roots, so a sign change there must come from the other polynomial of the pencil — the seed of alternation.

Counting roots from sign changes

theorem MSS.card_roots_ge_of_alternating (h : Polynomial ℝ) (hh : h ≠ 0) (n : ℕ) (x : Fin (n + 1) → ℝ) (hmono : StrictMono x) (halt : ∀ (i : Fin n), Polynomial.eval (x i.castSucc) h * Polynomial.eval (x i.succ) h < 0) : n ≤ h.roots.toFinset.card

Sign-change root count — the key lemma. If a real polynomial h takes values of strictly alternating sign at n+1 strictly increasing points x₀ < x₁ < … < xₙ (i.e. h(xᵢ)·h(xᵢ₊₁) < 0 for each consecutive pair), then it has at least n distinct real roots.

This is the heart of the Hermite–Kakeya–Obreschkoff argument and is not in Mathlib. The proof needs no list induction: each gap (xᵢ, xᵢ₊₁) independently yields a root by the IVT atom (exists_isRoot_of_eval_mul_neg, selected with choose), and the roots are pairwise distinct because they sit in disjoint, linearly ordered intervals (rᵢ < xᵢ₊₁ ≤ xⱼ < rⱼ for i < j). Injectivity then gives n ≤ #{distinct roots}.

theorem MSS.realRooted_of_alternating (h : Polynomial ℝ) (hh : h ≠ 0) (n : ℕ) (hdeg : h.natDegree ≤ n) (x : Fin (n + 1) → ℝ) (hmono : StrictMono x) (halt : ∀ (i : Fin n), Polynomial.eval (x i.castSucc) h * Polynomial.eval (x i.succ) h < 0) : RealRooted h

Sign-change real-rootedness. A polynomial of degree at most n that alternates sign at n+1 increasing points is real-rooted: the key lemma plus the counting lemma. This is the exact shape in which HKO concludes that a combination a·f + b·g is real-rooted — once the interlacing geometry supplies the alternating evaluation points.

Producing the alternation (the last span)

theorem MSS.eval_comb_at_isRoot (a b : ℝ) (f : Polynomial ℝ) {g : Polynomial ℝ} {s : ℝ} (hg : g.IsRoot s) : Polynomial.eval s (Polynomial.C a * f + Polynomial.C b * g) = a * Polynomial.eval s f

At a root s of the interlacer g, the combination a·f + b·g collapses to the scalar multiple a · f(s) (since g(s) = 0). This is the algebraic hinge that transfers f's sign pattern to the combination.

theorem MSS.comb_alternates_of_alternates (a b : ℝ) (ha : a ≠ 0) (f g : Polynomial ℝ) (n : ℕ) (s : Fin (n + 1) → ℝ) (hs : ∀ (j : Fin (n + 1)), g.IsRoot (s j)) (halt : ∀ (j : Fin n), Polynomial.eval (s j.castSucc) f * Polynomial.eval (s j.succ) f < 0) (j : Fin n) : Polynomial.eval (s j.castSucc) (Polynomial.C a * f + Polynomial.C b * g) * Polynomial.eval (s j.succ) (Polynomial.C a * f + Polynomial.C b * g) < 0

Alternation transfer. If f takes strictly alternating signs at points sⱼ that are all roots of g, and a ≠ 0, then the combination a·f + b·g also alternates there: at each sⱼ the combination equals a·f(sⱼ), so the consecutive product picks up a factor a² > 0 and keeps the sign of f's. This is "producing the alternation" for the combination.

theorem MSS.realRooted_comb_of_alternates (a b : ℝ) (ha : a ≠ 0) (f g : Polynomial ℝ) (n : ℕ) (hne : Polynomial.C a * f + Polynomial.C b * g ≠ 0) (hdeg : (Polynomial.C a * f + Polynomial.C b * g).natDegree ≤ n) (s : Fin (n + 1) → ℝ) (hmono : StrictMono s) (hs : ∀ (j : Fin (n + 1)), g.IsRoot (s j)) (halt : ∀ (j : Fin n), Polynomial.eval (s j.castSucc) f * Polynomial.eval (s j.succ) f < 0) : RealRooted (Polynomial.C a * f + Polynomial.C b * g)

Real-rootedness of a combination from a common interlacer's roots. If f alternates sign at n + 1 strictly increasing roots of g, and the combination a·f + b·g (nonzero, a ≠ 0) has degree ≤ n, then it is real-rooted. This is the Hermite–Kakeya–Obreschkoff conclusion, assembled from the key lemma (realRooted_of_alternating) and the alternation transfer — reducing the entire bridge to the single geometric input below.

theorem MSS.eval_mul_pos_of_no_isRoot (f : Polynomial ℝ) {u v : ℝ} (huv : u ≤ v) (hno : ∀ z ∈ Set.Icc u v, ¬f.IsRoot z) : 0 < Polynomial.eval u f * Polynomial.eval v f

Sign stability — the cornerstone of alternation. A polynomial with no root anywhere on a closed interval [u, v] keeps a constant nonzero sign there: f(u)·f(v) > 0. This is the contrapositive of the IVT atom and the local fact that turns "exactly one root of f per gap of g" into the sign flip that drives the whole interlacing alternation.

theorem MSS.eval_mul_neg_of_factor (q : Polynomial ℝ) {r u v : ℝ} (hur : u < r) (hrv : r < v) (hno : ∀ z ∈ Set.Icc u v, ¬q.IsRoot z) : Polynomial.eval u ((Polynomial.X - Polynomial.C r) * q) * Polynomial.eval v ((Polynomial.X - Polynomial.C r) * q) < 0

Sign flip across a lone root — the analytic last lemma. If f factors as (X - r)·q with the cofactor q having no root on [u, v] and u < r < v, then f flips sign across r: f(u)·f(v) < 0. Combined with sign stability this is the complete local content of interlacing alternation — f changes sign exactly across the single root sitting in each gap of the interlacer g.

theorem MSS.eval_alternating_of_factor_per_gap (f : Polynomial ℝ) (n : ℕ) (x : Fin (n + 1) → ℝ) (hfac : ∀ (i : Fin n), ∃ (r : ℝ) (q : Polynomial ℝ), x i.castSucc < r ∧ r < x i.succ ∧ f = (Polynomial.X - Polynomial.C r) * q ∧ ∀ z ∈ Set.Icc (x i.castSucc) (x i.succ), ¬q.IsRoot z) (i : Fin n) : Polynomial.eval (x i.castSucc) f * Polynomial.eval (x i.succ) f < 0

HKO assembly — the alternation, assembled. If f factors, across each gap (xᵢ, xᵢ₊₁) of a sequence, as (X - rᵢ)·qᵢ with the root rᵢ inside the gap and the cofactor qᵢ having no root on the closed gap — exactly the data a common interlacer supplies (one simple root of f per gap) — then f takes strictly alternating signs at the xᵢ. Immediate from the sign-flip lemma applied in each gap.

theorem MSS.realRooted_of_factor_per_gap (f : Polynomial ℝ) (hf0 : f ≠ 0) (n : ℕ) (hdeg : f.natDegree ≤ n) (x : Fin (n + 1) → ℝ) (hmono : StrictMono x) (hfac : ∀ (i : Fin n), ∃ (r : ℝ) (q : Polynomial ℝ), x i.castSucc < r ∧ r < x i.succ ∧ f = (Polynomial.X - Polynomial.C r) * q ∧ ∀ z ∈ Set.Icc (x i.castSucc) (x i.succ), ¬q.IsRoot z) : RealRooted f

Per-gap factorisation ⟹ real-rooted (the analytic heart of HKO). A polynomial of degree ≤ n with a simple root in each of n gaps of a strictly increasing sequence is real-rooted. Combines the assembly (eval_alternating_of_factor_per_gap) with the sign-change key lemma (realRooted_of_alternating). This closes the analytic content of "interlacing ⟹ real-rooted": once a common interlacer supplies the gaps and the per-gap factorisations, real-rootedness follows — the engine of Heilmann–Lieb.

Packaging: from "unique simple root in a gap" to the per-gap factorisation

theorem MSS.factor_of_unique_simple_root_on_Icc (f : Polynomial ℝ) (hf : f ≠ 0) {u v r : ℝ} (hr : f.IsRoot r) (hsimple : Polynomial.rootMultiplicity r f = 1) (huniq : ∀ z ∈ Set.Icc u v, f.IsRoot z → z = r) : ∃ (q : Polynomial ℝ), f = (Polynomial.X - Polynomial.C r) * q ∧ ∀ z ∈ Set.Icc u v, ¬q.IsRoot z

Per-gap factorisation from a unique simple root. If r ∈ [u,v] is a simple root of f (rootMultiplicity = 1) and the only root of f on [u,v], then f = (X − r)·q with the cofactor q root-free on [u,v]. This is the combinatorial packaging step that feeds realRooted_of_factor_per_gap: a root-free cofactor would force a double root at r (contradicting simplicity) or a second root in the gap (contradicting uniqueness).

theorem MSS.unique_simple_root_per_gap (f : Polynomial ℝ) (hf : f ≠ 0) (n : ℕ) (hdeg : f.natDegree ≤ n) (x : Fin (n + 1) → ℝ) (hmono : StrictMono x) (hroot : ∀ (i : Fin n), ∃ (r : ℝ), x i.castSucc < r ∧ r < x i.succ ∧ f.IsRoot r) (i : Fin n) : ∃ (r : ℝ), x i.castSucc < r ∧ r < x i.succ ∧ f.IsRoot r ∧ Polynomial.rootMultiplicity r f = 1 ∧ ∀ z ∈ Set.Icc (x i.castSucc) (x i.succ), f.IsRoot z → z = r

Counting: one root per gap ⟹ exactly one, simple, unique. A polynomial f ≠ 0 of degree ≤ n with at least one root in each of the n disjoint open gaps (xᵢ, xᵢ₊₁) of a strictly increasing sequence has, in each gap, exactly one root — simple and the only root of f on the closed gap. The n gap-roots are distinct (disjoint increasing gaps), so f has ≥ n distinct roots; with card roots ≤ deg ≤ n they account for everything, each simple. Combined with factor_of_unique_simple_root_on_Icc this supplies the data realRooted_of_factor_per_gap needs.

theorem MSS.realRooted_of_root_per_gap (f : Polynomial ℝ) (hf : f ≠ 0) (n : ℕ) (hdeg : f.natDegree ≤ n) (x : Fin (n + 1) → ℝ) (hmono : StrictMono x) (hroot : ∀ (i : Fin n), ∃ (r : ℝ), x i.castSucc < r ∧ r < x i.succ ∧ f.IsRoot r) : RealRooted f

Geometric interlacing ⟹ real-rooted — the engine, assembled. A polynomial f ≠ 0 of degree ≤ n with at least one root in each of the n gaps of a strictly increasing sequence is real-rooted. Chains the packaging (unique_simple_root_per_gap → factor_of_unique_simple_root_on_Icc) into the analytic engine (realRooted_of_factor_per_gap). Once a common interlacer supplies one root of f per gap, real-rootedness follows.

The recurrence step X·p − q (Hermite–Biehler) — algebraic hinge

theorem MSS.eval_X_mul_sub_at_isRoot (p q : Polynomial ℝ) {s : ℝ} (hs : p.IsRoot s) : Polynomial.eval s (Polynomial.X * p - q) = -Polynomial.eval s q

The recurrence collapses at a root of p. (X·p − q)(s) = −q(s) when p(s) = 0. The combination X·p − q is the matching/orthogonal-polynomial three-term recurrence shape; at the roots of p it reads off −q, transferring q's sign pattern.

theorem MSS.eval_X_mul_sub_mul_at_isRoots (p q : Polynomial ℝ) {s t : ℝ} (hs : p.IsRoot s) (ht : p.IsRoot t) : Polynomial.eval s (Polynomial.X * p - q) * Polynomial.eval t (Polynomial.X * p - q) = Polynomial.eval s q * Polynomial.eval t q

X·p − q inherits q's alternation at p's roots. On two roots s, t of p, (X·p−q)(s)·(X·p−q)(t) = q(s)·q(t) (each factor is −q, the signs square out). So if q alternates at consecutive roots of p — the geometric content of "q interlaces p" — then so does X·p − q, which is exactly the input realRooted_of_alternating needs to conclude X·p − q is real-rooted (the Hermite–Biehler recurrence step, modulo the ±∞ end gaps).

The ±∞ end gaps (the two outer alternation points of the recurrence step)

theorem MSS.exists_gt_forall_isRoot (f : Polynomial ℝ) (hf : f ≠ 0) : ∃ (x : ℝ), ∀ (y : ℝ), f.IsRoot y → y < x

A concrete point strictly above every root of f ≠ 0 (roots are finite, hence bounded).

theorem MSS.exists_lt_forall_isRoot (f : Polynomial ℝ) (hf : f ≠ 0) : ∃ (x : ℝ), ∀ (y : ℝ), f.IsRoot y → x < y

A concrete point strictly below every root of f ≠ 0.

theorem MSS.exists_gt_roots_eval_pos (f : Polynomial ℝ) (hf : f ≠ 0) (hlc : 0 < f.leadingCoeff) : ∃ (x : ℝ), (∀ (y : ℝ), f.IsRoot y → y < x) ∧ 0 < Polynomial.eval x f

Right end gap. Beyond all roots, f (positive leading coeff) is positive: a concrete x above every root with 0 < f(x). The right outer alternation point of realRooted_of_root_per_gap.

theorem MSS.exists_lt_roots_negOnePow_eval_pos (f : Polynomial ℝ) (hf : f ≠ 0) (hlc : 0 < f.leadingCoeff) : ∃ (x : ℝ), (∀ (y : ℝ), f.IsRoot y → x < y) ∧ 0 < ↑↑(↑f.natDegree).negOnePow * Polynomial.eval x f

Left end gap. Below all roots, f (positive leading coeff) has sign (−1)^{deg f}: a concrete x below every root with 0 < (−1)^{deg f}·f(x). The left outer alternation point.

Roots as a strictly increasing indexed family

theorem MSS.exists_strictMono_roots (p : Polynomial ℝ) (hp : p ≠ 0) : ∃ (k : ℕ) (s : Fin k → ℝ), StrictMono s ∧ (∀ (i : Fin k), p.IsRoot (s i)) ∧ ∀ (x : ℝ), p.IsRoot x → ∃ (i : Fin k), s i = x

The distinct roots of p ≠ 0, indexed in increasing order. Packages rootsList p as a StrictMono family Fin k → ℝ hitting exactly the roots — the inner points of the m+2-point sequence in the Hermite–Biehler assembly of hl_interlacing_recurrence.

theorem MSS.isRoot_eq_gap_root {f : Polynomial ℝ} (hf : f ≠ 0) {n : ℕ} (hdeg : f.natDegree ≤ n) {x : Fin (n + 1) → ℝ} (hmono : StrictMono x) {r : Fin n → ℝ} (hr1 : ∀ (i : Fin n), x i.castSucc < r i) (hr2 : ∀ (i : Fin n), r i < x i.succ) (hr3 : ∀ (i : Fin n), f.IsRoot (r i)) {z : ℝ} (hz : f.IsRoot z) : ∃ (i : Fin n), z = r i

Every root is a gap root. With one root r i per gap and deg f ≤ n, the n gap roots are all the roots of f: any root z equals some r i. (The r i are distinct and number n = #gaps; card roots ≤ deg ≤ n forces equality of root sets.) Used to confine q's roots to the interior, fixing its extreme signs in the Hermite–Biehler endpoint gaps.

theorem MSS.strictMono_extend {m : ℕ} (s : Fin m → ℝ) (hs : StrictMono s) (xL xR : ℝ) (hL : ∀ (i : Fin m), xL < s i) (hR : ∀ (i : Fin m), s i < xR) (hLR : xL < xR) : StrictMono (Fin.cons xL (Fin.snoc s xR))

Extend an increasing root family by two outer endpoints. Given a strictly increasing s : Fin m → ℝ with every value in (xL, xR), the sequence xL, s_0, …, s_{m-1}, xR is strictly increasing. The m+2-point sequence of the Hermite–Biehler assembly; strictMono reduces (via strictMono_iff_lt_succ) to the m+1 consecutive-gap inequalities.