Interlacing and the recurrence X p - q #
Polynomial lemmas for the interlacing form of the Heilmann–Lieb argument, where p = μ(G - a) and
q is a sum of matching polynomials of G - a - b. If q takes opposite signs at any two adjacent
roots of p (GeomInterlaced q p) and the roots of p are simple, then X p - q is real-rooted,
has a root in each gap between consecutive roots of p and one beyond each end, and p interlaces
it in turn. Everything is stated in ℝ[X].
Main definitions #
SimpleGraph.GeomInterlaced q p:qhas opposite signs at adjacent roots ofp.SimpleGraph.SignedGeomInterlaced q p: at each rootsofp,q(s)has the sign of(-1)^{#roots of p above s}; closed under sums.
Main results #
SimpleGraph.realRooted_X_mul_sub:X p - qis real-rooted.SimpleGraph.hl_geom_recurrence,SimpleGraph.hl_geom_recurrence_full: the recurrence step preserves interlacing.SimpleGraph.eval_negOnePow_card_above_pos: the sign of a real-rooted polynomial with positive leading coefficient at a non-rootxis(-1)^{#roots above x}.
References #
- O. J. Heilmann, E. H. Lieb, Theory of monomer-dimer systems, Comm. Math. Phys. 25 (1972) 190–232.
- S. Fisk, Polynomials, roots, and interlacing, arXiv:math/0612833.
Geometric route (skips the HKO bridge) #
Geometric interlacing — the HL-route invariant. q interlaces p geometrically: it
takes strictly opposite signs across any two adjacent roots of p (roots with no root of p
strictly between). The recurrence step uses realRooted_of_root_per_gap,
eval_X_mul_sub_at_isRoot, the ±∞ end gaps and exists_strictMono_roots.
Equations
- SimpleGraph.GeomInterlaced q p = ∀ (s t : ℝ), p.IsRoot s → p.IsRoot t → s < t → (∀ (z : ℝ), s < z → z < t → ¬p.IsRoot z) → Polynomial.eval s q * Polynomial.eval t q < 0
Instances For
Signed geometric interlacing — the additive, phase-locked refinement. At every root s
of p, q(s) carries the fixed sign of (-1)^{#roots of pstrictly aboves}. Unlike
GeomInterlaced (sign-agnostic per gap, so not closed under +), the phase is pinned, so a sum
of signed interlacers is one (SignedGeomInterlaced.add/.sum) — exactly what the matching
recurrence's q = Σ_{b∼a} μ(G⟦≠a,≠b⟧) needs. It implies GeomInterlaced when p has simple
roots (geomInterlaced), feeding hl_geom_recurrence. The phase matches a real-rooted positive-
leading interlacer's actual sign, so it is what the induction can establish from below.
Equations
- SimpleGraph.SignedGeomInterlaced q p = ∀ (s : ℝ), p.IsRoot s → 0 < Polynomial.eval s q * (-1) ^ (Multiset.filter (fun (x : ℝ) => s < x) p.roots).card
Instances For
A sum of two signed interlacers is a signed interlacer (the phase is pinned).
A nonempty finite sum of signed interlacers is a signed interlacer.
A signed interlacer is nonzero (it has a strict sign at each root of p, provided p has one).
Signed ⟹ geometric (for simple-rooted p). Across adjacent roots s < t the phase flips
exactly once (one fewer root lies above t than above s, and t is simple), so q(s)·q(t) < 0.
Internal-gap root of the recurrence (HKO-free, no Fin). Between two adjacent roots
s<t of p (no root of p strictly between), the recurrence combination X·p − q has a root.
Proof: (X·p−q)(s)·(X·p−q)(t) = q(s)·q(t) < 0 (the hinge eval_X_mul_sub_mul_at_isRoots plus
GeomInterlaced), so the intermediate-value theorem exists_isRoot_of_eval_mul_neg gives a root
in (s,t). This is the inner half of the input to realRooted_of_root_per_gap.
The recurrence step, assembled. Given p's roots as a full increasing family
s : Fin m → ℝ (m ≥ 1), two outer points xL < s_i < xR, q geometrically interlacing p,
and a root of X·p − q in each end gap (xL, s_0) and (s_{m-1}, xR) (phrased index-free via
∀ i, r < s i / ∀ i, s i < r), the recurrence combination X·p − q is real-rooted. The inner
gaps get their roots from exists_root_X_mul_sub_between_adjacent; the sequence is
strictMono_extend; the conclusion is realRooted_of_root_per_gap. This is the full
Hermite–Biehler assembly, with only the two end-gap roots left as hypotheses (the endpoint
parity, derivable from leading-coeff/degree data).
q's roots are confined to p's interior. With q geometrically interlacing p (roots
s : Fin (k+1), surjective) and deg q ≤ k, every root of q is < s_{last} and > s_0. Proof:
q has a root in each of the k gaps (alternation + IVT), and isRoot_eq_gap_root makes those
all of q's roots, each strictly inside (s_0, s_{last}).
Right end-gap root. X·p − q has a root above all of p's roots: q(s_{last})>0 (since
all q-roots are < s_{last}, by q_isRoot_lt_last), so (X·p−q)(s_{last})=−q(s_{last})<0, while
X·p − q is eventually positive (positive leading coeff); IVT gives the root.
q's roots exceed s_0 (mirror of q_isRoot_lt_last).
Left end-gap root. X·p − q has a root below all of p's roots. Here the signs carry a
parity: with deg q + 1 = deg p the degrees deg(X·p−q)=deg p+1 and deg q have equal parity,
so the (−1)^{deg} factors of the eventual signs of X·p−q (below all its roots) and of q (at
s_0, since all q-roots exceed s_0) cancel, giving opposite signs of X·p − q at the two ends
of the gap; IVT gives the root.
The geometric Hermite–Biehler recurrence step. Given p's roots as a full
increasing family s : Fin (k+1), q geometrically interlacing p with deg q + 1 = deg p and
nonnegative leading coefficients, the recurrence combination X·p − q is real-rooted. Assembles
the two end-gap roots (exists_left_end_root/exists_right_end_root) with the inner-gap engine
(realRooted_X_mul_sub). This is hl_geom_recurrence_target discharged (HKO-free).
Per-gap root of X·p − q (the extracted body of realRooted_X_mul_sub). Each of the
m+1 gaps of the sequence xL < s₀ < … < s_{m-1} < xR contains a root of X·p − q: the two end
gaps from hLend/hRend, the inner gaps from exists_root_X_mul_sub_between_adjacent. Factored
out so both realRooted_X_mul_sub (real-rootedness) and rootFamily_X_mul_sub (the simple root
family + interlacing) can consume it.
The X·p − q root family — m+1 simple roots, strictly interleaving p's m roots.
From exists_root_per_gap_X_mul_sub upgraded by unique_simple_root_per_gap: each gap yields a
unique simple root r i, the family is strictly increasing, and p's root s j sits strictly
between r jᶜ and r jˢ (r jᶜ < s j < r jˢ). Plus surjectivity onto the roots of X·p − q.
This is the geometric scaffold PIECE 2 needs to read off both simple-rootedness and interlacing
of the recurrence result.
Sign of a product ∏(x − aᵢ). Over a root-free point x (no aᵢ = x), the product
∏_{a∈M}(x − a) carries the sign (−1)^{#{a : x < a}} — one sign flip per factor with a > x.
The combinatorial seed of the "sign of a real-rooted polynomial" formula.
Sign of a real-rooted polynomial between its roots. For a real-rooted p with positive
leading coefficient and x not a root, p(x)·(−1)^{#{roots > x}} > 0: the sign of p(x) is
(−1)^{number of roots above x} (times the positive leading sign). Factor p = lc·∏(X − rᵢ) (it
splits) and apply prod_map_sub_negOnePow_pos. This is the absolute-sign input the signed
interlacing phase needs.
The roots of a real-rooted, simple-rooted polynomial are its root family. If t : Fin n
is strictly monotone, lands on roots, is surjective onto them, each simple, and g has n roots,
then g.roots = (Finset.univ.val).map t as a multiset. Lets root-count filters be computed over
Fin n.
PIECE 2 — p geometrically interlaces X·p − q. Between two adjacent roots u < v of
X·p − q sits exactly one root s j of p, simple, so p changes sign once across (u,v):
p(u)·p(v) < 0. Uses the rootFamily_X_mul_sub scaffold (adjacent X·p−q-roots are consecutive
r i, r (i+1), with s i interleaved) + factor_of_unique_simple_root_on_Icc +
eval_mul_neg_of_factor. Combined with hl_geom_recurrence's real-rootedness this discharges the
full hl_geom_recurrence_target.
PIECE 2, SIGNED — p signed-geometrically interlaces X·p − q. Strengthens
geomInterlaced_X_mul_sub to the phase-pinned predicate SignedGeomInterlaced p (X·p − q),
which (unlike the unsigned one) is closed under + — exactly what the |V|-induction needs for
q = Σ_{b∼a} μ(G⟦≠a,≠b⟧). At an f-root r i the phase (−1)^{#f-roots above r i} equals
(−1)^{#p-roots above r i} (both count m − i, via the strict interleaving r jᶜ < s j < r jˢ),
and eval_negOnePow_card_above_pos gives 0 < p(r i)·(−1)^{#p-roots above}. Needs p monic-ish
(0 < leadingCoeff) + real-rooted with m roots.
The full geometric Hermite–Biehler step — the inductive payload (PIECE 2 + recurrence).
Given p real-rooted with simple roots and q geometrically interlacing p (matching-recurrence
degree/leading data), X·p − q is (1) real-rooted, (2) geometrically interlaced by p, and (3)
all its roots are simple. This is exactly the triple the |V|-induction carries
(HLGeom_target-style invariant): real-rootedness propagates, p = μ(G∖a) interlaces μ(G), and
μ(G) stays simple-rooted. Assembles hl_geom_recurrence (real) + geomInterlaced_X_mul_sub
(interlacing) + rootFamily_X_mul_sub (simple), sharing the end-gap roots.
Base case — re-export. μ(⊥) is real-rooted, anchoring the interlacing induction.