Summary
We should add a Lean-facing interface for the finite-degree
Borcea--Branden algebraic-symbol theorem, with a clear warning that proving the
theorem itself is substantial work.
The intended theorem is the finite-degree real-rootedness-preserver criterion:
for a real linear operator T : ℝ[X] →ₗ[ℝ] ℝ[X] acting on polynomials of degree
at most d, the stability of the algebraic symbol
implies that T preserves real-rootedness in degree <= d (up to the zero
polynomial). This is the direction of the Borcea--Branden classification that
is most useful for coefficient-operator tactics.
Reference:
- J. Borcea and P. Branden, The Lee-Yang and Polya-Schur programs. I.
Linear operators preserving stability, Invent. Math. 177 (2009), 541--569.
- P. Branden, Unimodality, log-concavity, real-rootedness and beyond,
Handbook of Enumerative Combinatorics.
Proposed first milestone
Add a module, perhaps under RealRooted/Stability/, that states the theorem as
a precise classical input, without trying to prove it immediately.
Possible shape:
def MvUpperHalfPlaneStable {sigma : Type*} (p : MvPolynomial sigma ℂ) : Prop :=
∀ z : sigma → ℂ, (∀ i, 0 < (z i).im) → MvPolynomial.eval z p ≠ 0
def PreservesRealRootedUpTo
(d : Nat) (T : ℝ[X] →ₗ[ℝ] ℝ[X]) : Prop :=
∀ {p : ℝ[X]}, p.natDegree ≤ d → p.Splits → T p = 0 ∨ (T p).Splits
def borceaBrandenFiniteSymbolStatement : Prop :=
∀ {d : Nat} {T : ℝ[X] →ₗ[ℝ] ℝ[X]},
MvUpperHalfPlaneStable (finiteAlgebraicSymbol d T) →
PreservesRealRootedUpTo d TThe exact names and binder style should be adjusted to match the local API.
Why this is useful
This would let tactic backends reduce concrete real-rootedness-preserver claims
to finite symbol stability checks. For example, coefficient-bidiagonal
operators have symbols of the form
sum_{k=0}^d binom(d,k) alpha_k x^k y^(d-k)
+ x * sum_{k=0}^d binom(d,k) beta_k x^k y^(d-k).
For quadratic coefficient sequences this symbol often factors as a power of
x+y times a low-degree homogeneous polynomial, so the remaining stability
check can be discharged by explicit low-degree certificates.
Warning
Fully proving the theorem is a serious formalization project. It likely needs:
- a multivariate upper-half-plane stability predicate;
- closure lemmas for stable multivariate polynomials;
- a finite algebraic-symbol API;
- bridges between univariate real-rootedness and bivariate stability;
- enough
MvPolynomial normalization support to make examples tractable;
- eventually, the finite-degree Borcea--Branden theorem itself.
The immediate value is to state the theorem precisely and use it as a named
classical interface, following the current project style for other deep
external inputs.
Summary
We should add a Lean-facing interface for the finite-degree
Borcea--Branden algebraic-symbol theorem, with a clear warning that proving the
theorem itself is substantial work.
The intended theorem is the finite-degree real-rootedness-preserver criterion:
for a real linear operator
T : ℝ[X] →ₗ[ℝ] ℝ[X]acting on polynomials of degreeat most
d, the stability of the algebraic symbolimplies that
Tpreserves real-rootedness in degree<= d(up to the zeropolynomial). This is the direction of the Borcea--Branden classification that
is most useful for coefficient-operator tactics.
Reference:
Linear operators preserving stability, Invent. Math. 177 (2009), 541--569.
Handbook of Enumerative Combinatorics.
Proposed first milestone
Add a module, perhaps under
RealRooted/Stability/, that states the theorem asa precise classical input, without trying to prove it immediately.
Possible shape:
The exact names and binder style should be adjusted to match the local API.
Why this is useful
This would let tactic backends reduce concrete real-rootedness-preserver claims
to finite symbol stability checks. For example, coefficient-bidiagonal
operators have symbols of the form
For quadratic coefficient sequences this symbol often factors as a power of
x+ytimes a low-degree homogeneous polynomial, so the remaining stabilitycheck can be discharged by explicit low-degree certificates.
Warning
Fully proving the theorem is a serious formalization project. It likely needs:
MvPolynomialnormalization support to make examples tractable;The immediate value is to state the theorem precisely and use it as a named
classical interface, following the current project style for other deep
external inputs.