Roadmap: Mathlib-oriented Borcea-Branden stability preservers

[PerAlexandersson]

Goal

Plan a Mathlib-shaped formalization route for Borcea--Branden stability-preserving
linear operators, starting from the theory already present in this repository.

This is broader than the closed finite-symbol scaffold in #69. The existing
#69 interface is useful, but it records only one application-facing direction:
for a univariate real operator, stability of T((x + y)^d) implies preservation
of real-rootedness up to degree d. The eventual API should support the actual
finite-dimensional Borcea--Branden classifications and later the transcendental
infinite-dimensional versions.

Primary source:

• J. Borcea and P. Branden, The Lee-Yang and Polya-Schur programs. I. Linear
  operators preserving stability, Invent. Math. 177 (2009), 541--569,
  arXiv:0809.0401, DOI: 10.1007/s00222-009-0189-3.

Existing local theory to preserve and reuse

The repository already has substantial pieces that should be treated as the
starting point.

• RealRooted/MultivariateStability.lean defines complexifyMv,
  MvUpperHalfPlaneStable, MvRealStable, affine-line restriction, and closure
  under nonzero scalar multiplication, multiplication, factors, renaming, and
  left/right specialization. It also contains the bivariate lift xyLift.
• RealRooted/Multiaffine.lean, RealRooted/LiebSokalOperator.lean, and
  RealRooted/LiebSokalPointwise.lean contain multiaffineness, the
  F(-partial){G} differential action, Gauss--Lucas-based derivative stability,
  specialization-at-zero, and the pointwise tools for the Lieb--Sokal theorem.
  These are core Borcea--Branden sufficiency ingredients, not side material.
• RealRooted/HermiteBiehler.lean defines separate univariate
  IsUpperHalfPlaneStable, right-half-plane and Hurwitz stability, plus many
  Hermite--Biehler/proper-position bridges. The future API should bridge this
  to, or gradually migrate it toward, the multivariate predicate instead of
  creating another competing stability vocabulary.
• RealRooted/HurwitzMatrix.lean records that the current row-oriented Hurwitz
  criterion attempts are false. A Borcea--Branden roadmap should not build on
  those false interfaces; if Hurwitz matrices are needed, first introduce the
  correctly oriented classical matrix and criterion.
• RealRooted/Challenges/BorceaBranden.lean is the State finite Borcea-Branden symbol theorem interface #69 challenge interface.
  Keep it as a compatibility/application wrapper until a general symbol theorem
  exists.
• RealRooted/Tactic/FiniteSymbolPF.lean and its frontends already implement a
  concrete coefficient-bidiagonal finite-symbol route with homogenized bivariate
  symbols and residual certificates. This should become an application layer
  depending on the general theorem.
• Related closed issues Formalize PPlus/nonnegative-root real-stability bridge #87, Formalize polarization preserves real stability #88, and Formalize Lieb-Sokal differential-operator stability theorem #89 already pushed useful pieces of the
  multivariate stability/polarization/Lieb--Sokal infrastructure.

Source theorem targets

The finite-dimensional targets from Borcea--Branden I should guide the API.

• Complex finite theorem, paper Theorem 1.1: for
  T : C_kappa[z] -> C[z], T preserves stability iff either the image has
  rank at most one and is generated by a stable polynomial, or the algebraic
  symbol G_T(z,w) = T((z + w)^kappa) is stable in the 2n variables.
• Real finite theorem, paper Theorem 1.2: for
  T : R_kappa[z] -> R[z], T preserves real stability iff either the image
  has rank at most two and is of the form alpha(f) P + beta(f) Q with P,Q
  real stable and in proper position, or G_T(z,w) is real stable, or
  G_T(z,-w) is real stable.
• Infinite-dimensional/transcendental analogues, paper Theorems 1.3 and 1.4,
  should be planned later. They require entire functions/Laguerre--Polya style
  limits and should not drive the first Lean definitions unless the finite API
  would otherwise become incompatible.

Definition decisions

These are the definitions to get right before proving large theorems.

1. Stability should keep the current nonzero convention.
   MvUpperHalfPlaneStable P := forall z, Im z_i > 0 -> eval z P != 0 makes
   0 not stable, matching the paper's preserver convention where the output is
   stable or zero. Add explicit zero-aware wrappers such as
   MvUpperHalfPlaneStableOrZero and MvRealStableOrZero; do not silently make
   zero stable.

2. Prefer an upstreamable namespace and hierarchy.
   Candidate shape:

   namespace MvPolynomial
   
   def StableIn (Omega : sigma -> Set C) (P : MvPolynomial sigma C) : Prop :=
     forall z, (forall i, z i in Omega i) -> eval z P != 0
   
   abbrev UpperHalfPlaneStable (P : MvPolynomial sigma C) : Prop :=
     StableIn (fun _ => {z | 0 < z.im}) P
   
   abbrev RealStable (P : MvPolynomial sigma R) : Prop :=
     UpperHalfPlaneStable (P.map Complex.ofRealHom)

   The local RealRooted.MvUpperHalfPlaneStable can remain as a compatibility
   alias during migration.

3. Keep real and complex stability separate.
   Complex stability should live over MvPolynomial sigma C; real stability is
   complex stability after coefficient embedding. Avoid statements that quantify
   over an arbitrary IsROrC field until the basic API is stable.

4. Add a finite box-degree submodule for multivariate polynomials.
   The Borcea--Branden domain is not total degree <= d; it is the box
   degreeOf i <= kappa i for every variable. Reuse Mathlib's existing
   submodule patterns: univariate work can use Polynomial.degreeLE/
   degreeLT, while the multivariate side should be a small upstreamable layer
   over MvPolynomial.restrictSupport, e.g.

   def MvPolynomial.degreeOfLE (R : Type*) [CommSemiring R]
       [Fintype sigma] (kappa : sigma -> Nat) :
       Submodule R (MvPolynomial sigma R) := ...

5. Define algebraic symbols by monomial expansion, not by ad hoc string or
   substitution tricks.
   For T : degreeOfLE R kappa ->_R MvPolynomial sigma R, define
   algebraicSymbol kappa T : MvPolynomial (sigma ⊕ sigma) R as the finite sum
   over alpha <= kappa of
   binom(kappa, alpha) * rename Sum.inl (T (X^alpha)) * X_right^(kappa-alpha).
   Then prove it equals the informal T((z+w)^kappa) formulation.

6. Include the sign-reversed real symbol from the beginning.
   The real theorem has a G_T(z,-w) alternative. Add a reusable operation
   such as negRightVariables or symbolNegRight, and prove it agrees with
   substituting -X in the right variable block.

7. Formalize multivariate proper position separately from the existing
   univariate Prec.
   In the paper, proper position is a stability condition on g + I * f.
   Add a multivariate predicate with the paper's orientation, then prove bridge
   lemmas to the current univariate Prec/Prec0 API only after checking the
   order/sign convention carefully.

8. Do not encode low-rank alternatives only as finrank range <= 1/2.
   For theorem statements and use, structures are clearer and easier to apply:

   structure ComplexRankOneStableRange ... :=
     (functional : V ->_C C)
     (P : MvPolynomial sigma C)
     (stable_P : UpperHalfPlaneStable P)
     (eq_map : forall f, T f = functional f * P)
   
   structure RealRankTwoProperPositionRange ... :=
     (alpha beta : V ->_R R)
     (P Q : MvPolynomial sigma R)
     (stable_P : RealStable P)
     (stable_Q : RealStable Q)
     (proper : ProperPosition P Q)
     (eq_map : forall f, T f = alpha f * P + beta f * Q)

   Later prove equivalences with rank bounds if useful.

9. Keep circular-domain generality out of the first implementation.
   A StableIn foundation can support circular domains later, but the first
   theorem should target upper-half-plane stability. This is where the current
   code and applications already live.

Proposed module split

Possible local modules, with upstream destinations in mind:

• RealRooted/Mathlib/Algebra/MvPolynomial/Stability/Basic.lean
  for StableIn, UpperHalfPlaneStable, RealStable, zero-aware wrappers,
  complexification simp lemmas, rename/specialization/product/scalar/factor
  closure.
• RealRooted/Mathlib/Algebra/MvPolynomial/Stability/DegreeBox.lean
  for the degreeOfLE box submodule, monomial basis helpers, and finite sums
  over alpha <= kappa.
• RealRooted/Mathlib/Algebra/MvPolynomial/Stability/Symbol.lean
  for algebraic symbols, sign-reversed symbols, and univariate specializations.
• RealRooted/Mathlib/Algebra/MvPolynomial/Stability/ProperPosition.lean
  for multivariate proper position and links to Hermite--Biehler/Obreschkoff.
• RealRooted/Mathlib/Algebra/MvPolynomial/Stability/Multiaffine.lean
  for upstreamable parts of the current Multiaffine and Lieb--Sokal algebra.
• RealRooted/BorceaBranden/Finite.lean
  for the theorem-shaped Borcea--Branden finite classifications and reductions.
• RealRooted/BorceaBranden/Applications/*.lean
  for PF-bidiagonal, Hermite--Poulain, Euler/operator-preserver, and tactic
  frontends that should not be upstreamed as core Mathlib API.

The exact filenames can change, but the core rule should be: upstreamable
vocabulary and closure lemmas go under RealRooted/Mathlib/...; theorem
scaffolds and applications stay under RealRooted/....

Milestones

1. Inventory and alias cleanup.
   List every local stability/proper-position notion and decide which are core,
   aliases, or application wrappers. In particular, bridge
   HermiteBiehler.IsUpperHalfPlaneStable to the multivariate one-variable
   predicate before adding new theorem statements.

2. Zero-aware stability API.
   Add UpperHalfPlaneStableOrZero/RealStableOrZero and refactor preserver
   definitions to use these wrappers. This should be a small PR with focused
   closure lemmas and no Borcea--Branden theorem proof attempt.

3. Box-degree API.
   Implement the bounded multivariate box submodule and helper lemmas for
   monomials, finite support, and coefficient expansion. Prove the univariate
   box agrees with Polynomial.degreeLE R d / degreeLT R (d+1) where needed.

4. Algebraic symbol API.
   Define the general finite algebraic symbol and the z,-w variant. Prove
   that the existing State finite Borcea-Branden symbol theorem interface #69 finiteAlgebraicSymbol and the tactic
   FiniteSymbolPF.finiteSymbol are specializations or application wrappers of
   the general definition.

5. Proper position API.
   Add multivariate proper position, real/complex component lemmas, and the
   univariate bridge to Prec/Prec0. This milestone should explicitly audit
   the orientation: the paper's f << g is defined via g + I*f stable, while
   current local notation has its own established order.

6. Closure theorem layer.
   Fill the Borcea--Branden Lemma 1.7-style closure facts needed by symbols:
   real specialization, positive rescaling, inversion/reversal, diagonalization,
   products, factors, and block-variable renaming. Reuse existing lemmas where
   possible instead of duplicating them under Borcea--Branden names.

7. Multiaffine/polarization/Lieb--Sokal layer.
   Consolidate the current closed-issue work (Formalize PPlus/nonnegative-root real-stability bridge #87--Formalize Lieb-Sokal differential-operator stability theorem #89): multiaffine predicates,
   polarization/projection operators, Grace--Walsh--Szego or a theorem-shaped
   interface for polarization preserving stability, and the Lieb--Sokal
   differential action. This is the core sufficiency route for the complex
   finite theorem.

8. State the full finite classification interfaces.
   Add theorem-shaped statements for Theorems 1.1 and 1.2 with all alternatives:
   complex rank-one or stable symbol; real rank-two proper-position image,
   stable symbol, or sign-reversed stable symbol. The existing State finite Borcea-Branden symbol theorem interface #69 theorem
   becomes a corollary/application, not the primary statement.

9. Prove finite-symbol sufficiency first.
   The first serious proof target should be the forward direction from stable
   symbol to stability preservation, since this directly supports the existing
   tactic applications. Use the multiaffine reduction and existing
   Lieb--Sokal infrastructure.

10. Add the real finite univariate corollaries.
    Derive the degree-d real-rootedness-preserver theorem used by State finite Borcea-Branden symbol theorem interface #69 and
    FiniteSymbolPF. Include the sign-reversed symbol and rank-two alternatives
    in the statement even if applications mostly use the positive symbol branch.

11. Only then consider necessity and transcendental theorems.
    Necessity uses Hurwitz-type limit arguments and the transcendental theorems
    require entire-function/Laguerre--Polya infrastructure. These should be
    separate issues after the finite API has stopped moving.

12. Application refactors.
    Migrate RealRooted/Tactic/FiniteSymbolPF.lean, Hermite--Poulain wrappers,
    Euler/operator-preserver wrappers, and any PF/Narayana uses onto the general
    symbol theorem. Keep tactic-specific residual certificates outside the
    upstreamable core.

First child issues to create from this roadmap

• Define zero-aware multivariate stability wrappers and bridge the univariate
  IsUpperHalfPlaneStable predicate to MvUpperHalfPlaneStable.
• Define MvPolynomial.degreeOfLE for box-bounded multivariate polynomials.
• Define general finite algebraic symbols and prove the existing univariate
  finiteAlgebraicSymbol is the Fin 1/Fin 2 specialization.
• Define multivariate proper position and bridge it to Prec/Prec0 in one
  variable.
• Restate Borcea--Branden finite Theorems 1.1 and 1.2 with all low-rank and
  symbol alternatives.
• Refactor FiniteSymbolPF to consume the general symbol API.

Risks and cautions

• Do not build on the row-oriented Hurwitz criterion interfaces as if they were
  true; the repository has checked counterexamples.
• Do not make 0 stable merely for convenience. Use explicit StableOrZero
  wrappers in preserver statements.
• Do not let the univariate Prec orientation leak into multivariate proper
  position without a checked sign/order bridge.
• Do not specialize the core definitions to bivariate/univariate tactic needs.
  The algebraic symbol should be multivariate from the start.
• Avoid circular-domain master-theorem generality until upper-half-plane
  stability is robust.
• Keep application certificates, OEIS/tactic frontends, and low-degree residual
  normalization out of the Mathlib-shaped core.

Acceptance criteria for the roadmap issue

This issue is done when the finite-dimensional Borcea--Branden theory is
represented by stable Lean interfaces and at least the positive-symbol
sufficiency branch has been proved or reduced to named standard inputs, with
existing #69 and FiniteSymbolPF applications using the general API rather than
parallel bespoke definitions.

[PerAlexandersson]

Additional local touchpoint map, following the note that a lot of theory already touches this roadmap.\n\nThis should be treated as a consolidation project, not a greenfield development. Beyond the modules named in the issue body, these existing files should influence the API boundaries:\n\n- RealRooted/OperatorPreservesInterlacing.lean already has the zero-aware linear-operator language PreservesRealRootedOrZero, PreservesAllComboPairs, and PreservesInterlacingPairsUpToOrder0. The Borcea--Branden preserver predicates should reuse this zero-or-stable convention rather than inventing a parallel one.\n- RealRooted/ObreschkoffConverse.lean and the new compatibility split in commit 94309e1 give the univariate bridge from real-rooted pencil preservation to oriented/unoriented interlacing. This is the local univariate shadow of the proper-position alternatives in Borcea--Branden.\n- RealRooted/Apolarity.lean and RealRooted/GraceHalfPlane.lean already contain finite apolarity and half-plane geometry. These are natural homes or dependencies for Grace--Walsh--Szego-style inputs used by polarization and stability preservers.\n- RealRooted/Polarization.lean, RealRooted/RectangularPolarization.lean, RealRooted/RectangularPolarizationComplement.lean, and RealRooted/MultiaffineReciprocal.lean already implement multiaffine polarization, rectangular two-block polarization, and reciprocal transforms preserving upper-half-plane stability. These should feed the multiaffine/polarization milestone directly.\n- RealRooted/MultiplierSequence.lean, RealRooted/PFPolynomial.lean, RealRooted/AissenSchoenbergWhitney*.lean, and RealRooted/Tactic/FiniteSymbolPF.lean are application/front-end layers for Polya--Schur/PF-style consequences. They should consume the eventual symbol theorem, but should not drive the core multivariate definitions.\n- RealRooted/HeilmannLieb.lean and the Lieb--Sokal files are stability-preserver examples/inputs; they are useful test cases for whether the general API is expressive enough.\n\nPractical consequence for this roadmap: first child issues should inventory and alias existing predicates before adding new theorem statements. In particular, connect OperatorPreservesInterlacing-style zero escape, HermiteBiehler proper-position vocabulary, and MultivariateStability predicates before defining the Borcea--Branden symbol-preserver structures.

[PerAlexandersson]

Follow-up after local repo audit plus a focused Claude review on 2026-07-31. The current roadmap is already detailed enough to serve as the parent issue; these are the definition-level constraints I would pin before creating child issues.

1. Make StableIn the only primitive. Keep UpperHalfPlaneStable and RealStable as abbrevs or compatibility aliases, not independent definitions with separate lemma families. Until the upstream shape is stable, avoid squatting directly in the public MvPolynomial namespace except in RealRooted/Mathlib/... files intended for extraction.

2. Choose coordinate-wise regions early. The useful general form is likely StableIn (Omega : sigma -> Set C), because existing nonzero-evaluation arguments need coordinate-wise infinitude hypotheses. A single Set (sigma -> C) is less convenient for rename, specialization, and half-plane transport lemmas.

3. Treat StableOrZero as a real API, not just a bare disjunction unfolded everywhere. The first child issue should include constructors, eliminators, and closure lemmas for scalar multiplication, multiplication, factors, renaming, specialization, derivatives where valid, and finite products. Stability remains the hypothesis primitive; StableOrZero is the preserver conclusion primitive.

4. For bounded domains, reuse Mathlib's existing uniform MvPolynomial.restrictDegree instead of redefining it. The new upstreamable work is the vector-box version degreeOf i <= kappa i, with membership lemmas via both support and degreeOf, monotonicity in kappa, compatibility with the uniform bound, and finite/basis results indexed by Pi i, Fin (kappa i + 1).

5. Make the Hermite--Biehler/proper-position bridge a prerequisite, not a later cleanup. The current univariate Prec API is combinatorial and oriented; the Borcea--Branden real theorem uses analytic proper position via stability of a complex combination. We need a checked orientation bridge, including the sign convention for f + I * g, the upper-half-plane convention, and the z,-w symbol branch.

6. If the low-rank alternatives are proof-carrying structures, give them an ergonomic API immediately: @[ext] lemmas, coercions or fields exposing the underlying linear map/functionals, and simp lemmas for the representation of T f. Otherwise every application will grow its own low-rank glue.

Suggested first child issue: consolidate the stability predicate layer before proving any Borcea--Branden theorem. That means StableIn, aliases for the current MvUpperHalfPlaneStable/MvRealStable, zero-aware wrappers with closure lemmas, and the one-variable bridge to HermiteBiehler.IsUpperHalfPlaneStable.

[PerAlexandersson]

Progress on the first stability-predicate milestone is now on main:

• ea2c44c adds MvUpperHalfPlaneStableOrZero, zero/stable constructors, arbitrary scalar multiplication, multiplication, and rename closure.
• c72ce0f adds strict stability of 1, finite-product closure, and zero-aware left/right block specialization.

This makes zero escape an explicit API rather than a repeatedly unfolded disjunction, while retaining strict MvUpperHalfPlaneStable as the input hypothesis primitive. The definitions and core closures compiled locally and were independently checked in Axle 4.31 (request ce504a1d-7f19-4835-ae7d-a105cbce070f).

Tactic consequence: future general finite-symbol/preserver infrastructure should return MvUpperHalfPlaneStableOrZero. Specialized finiteSymbolBBStatement currently concludes BidiagonalPFPreserver, so it should consume the zero-aware core theorem internally rather than changing its public specialized target without a separate API review.

[PerAlexandersson]

The coordinate-wise stability milestone has advanced on main:

• f13f6be makes MvStableIn (Omega : sigma → Set ℂ) the underlying primitive and adds generic MvStableInOrZero, while retaining opaque upper-half-plane compatibility wrappers plus simp bridges.
• 7fd965d adds generic region APIs for stable 1, scalar multiplication, multiplication, finite products, and region-compatible renaming, together with zero-aware variants.

The wrappers are deliberately opaque rather than abbrev: fully reducible aliases caused receiver-style calls such as hP.mul to resolve against Function.mul. The simp bridge theorems preserve easy conversion to the generic predicates without breaking the existing API.

Both modules compiled locally; Axle independently checked the primitive compatibility and generic closure proofs.

[PerAlexandersson]

Commit 9d5ad48 extends the coordinate-wise stability milestone with:

• MvStableIn.left_of_mul and right_of_mul;
• strict and zero-aware specializeRight for Sum.elim Omega Psi;
• strict and zero-aware specializeLeft for the same block-region structure.

This supplies the generic block-specialization API needed when a finite symbol is stable-or-zero in input/output variable blocks. The owning module compiles locally.

[PerAlexandersson]

Progress update:

• 77c4000 simplifies Polynomial.homogenize_rootFactorProduct using the induction proof returned by Aristotle, after manual review and local Lean compilation. Aristotle project/task: a7e42e63-1c63-4fd2-99e4-81e6159cc6a9 / 50566a2c-f518-4b8e-bcb1-c3ccd171d0fa.
• eee246c generalizes nonzero evaluation from the upper half-plane to arbitrary coordinate-wise infinite regions via exists_stableIn_eval_ne_zero; the upper-half-plane result is now a corollary. Axle request: 58811948-ff34-4f2c-b568-f84649a5645f.
• These are foundational API steps toward the finite-symbol route. They do not replace any remaining theorem by an opaque proposition or an admitted proof. Where a later theorem needs a purely combinatorial interpretation, that boundary will remain an explicit hypothesis with a nearby comment explaining why it is intentionally assumed; real-rootedness/stability consequences will still be derived formally from the recurrences.

The finite-symbol theorem itself remains the main analytic gap. Erik’s current refactor PRs still need checked proofs rather than by sorry.

[PerAlexandersson]

Main regression fix: 0405da4 restores Polarization.lean after the coordinate-wise stability refactor by explicitly converting z i ∈ lowerHalf 0 to the underlying imaginary-part inequality before applying not_le_of_gt. The focused module compiles under Lean 4.31. This was exposed by PR #252's aggregate comparator build and is independent of that PR's rejected by sorry conversion.

[PerAlexandersson]

Finite-symbol/Jensen roadmap correction:

• The current homogeneous FiniteSymbolPF.finiteSymbol premise does not imply PF preservation. At d=1, alpha=[1,0], beta=[2,1], its symbol is (X+Y)^2, but 1+2X maps to non-real-rooted 1+2X+2X^2 (discriminant -4).
• The counterexample is checked by polytool and Axle and recorded in polynomial-lab project realrooted_finite_symbols.
• Main commit 9179f46 now computes the genuine affine algebraic symbol exactly as affineBidiagonalSymbol.
• Remaining valid tasks are genuine affine finite-symbol sufficiency and a separate Jensen-certificate-to-affine-stability theorem. Tactic backends must remain explicit until both are checked.