Generalize Grace polarization stability to degree at most n

[PerAlexandersson]

Problem

Borcea--Branden I, Proposition 2.4 and Lemma 2.5 require polarization in a source variable of degree at most n to preserve upper-half-plane stability. The current Lean theorem

theorem mvUpperHalfPlaneStable_polarization
    (hdeg : p.natDegree = n)
    (hstable : ∀ w : ℂ, 0 < w.im → p.eval w ≠ 0) :
    MvUpperHalfPlaneStable (polarization n p)

only handles exact degree. This is insufficient for output-parametric source polarization: specializing the output variables can lower the source degree.

This blocks the stability-transfer step in #297 / PR #301 after the full Lemma 2.5 algebraic-symbol identity.

Source

• Borcea and Branden, The Lee--Yang and Polya--Schur Programs. I, arXiv:0809.0401, Proposition 2.4, equation (2.2), and Lemma 2.5.
• The project proof is in RealRooted/Polarization.lean.
• The Grace lower-half-plane induction is in RealRooted/GraceHalfPlane.lean.

Exact missing theorem

Generalize the first-degree premise of

grace_apolarity_lowerHalf

from

(binomialLift n f).natDegree = n

to

(binomialLift n f).natDegree ≤ n

while retaining exact degree n for binomialLift n g. The second equality is still needed for root existence and deflation.

Then expose:

theorem mvUpperHalfPlaneStable_polarization
    {n : ℕ} {p : ℂ[X]}
    (hdeg : p.natDegree ≤ n)
    (hstable : ∀ w : ℂ, 0 < w.im → p.eval w ≠ 0) :
    MvUpperHalfPlaneStable (polarization n p)

Paper-faithful proof route

1. Generalize the first-polynomial invariant in grace_aux_lowerHalf to degree at most n.
2. Prove the bounded recursive estimate
   (polarDeriv n ζ A).natDegree ≤ n - 1 from A.natDegree ≤ n.
3. Preserve root containment under the same polar-derivative step.
4. Keep the second polynomial at exact degree throughout the induction.
5. Update mvUpperHalfPlaneStable_reducedPolarization; its exact-degree hypothesis is used only when calling Grace.
6. Update the polarization wrapper using existing binomialLift_binomialUnlift hdeg.

Existing bounded support facts include natDegree_binomialLift_le and binomialLift_binomialUnlift; do not add an unproved statement or an exact-degree specialization assumption.

Acceptance criteria

• The bounded-degree Grace theorem is fully proved.
• The degree-at-most polarization stability theorem is fully proved.
• Existing exact-degree call sites continue to work via .le or a compatibility wrapper.
• Add focused tests/examples for a stable polynomial of degree strictly below n.

[PerAlexandersson]

First prerequisite landed on PR #301 as commit 8fc0d732: polarDeriv_natDegree_le proves purely algebraically that A.natDegree ≤ n and 1 ≤ n imply (polarDeriv n ζ A).natDegree ≤ n - 1. AXLE verified the exact Lean 4.31 proof without warnings. The next step is the genuinely analytic bounded-degree root-containment lemma; the current reciprocal-average proof identifies n with the number of finite roots and therefore cannot simply reuse the exact-degree theorem.

[PerAlexandersson]

Commit c958eb8e proves the missing analytic geometry. mem_lowerHalf_of_recip_sum_of_card_le handles numerator n ≥ S.card by introducing the scaled pole ζ' = w - (S.card/n)(w-ζ) and applying the existing exact-card reciprocal-average theorem. polarDeriv_rootsIn_lowerHalf_of_natDegree_le then handles constants directly and positive degree via roots.card = natDegree ≤ n. Both proof cores were AXLE-checked under Lean 4.31 without warnings. The next edit is now mechanical: thread ≤ only for the first polynomial through grace_aux_lowerHalf.

[PerAlexandersson]

Implemented the lower-half-plane prerequisite in commit a843543 (PR #301).

The Grace induction now assumes (binomialLift n f).natDegree ≤ n for its first polynomial and retains (binomialLift n g).natDegree = n for the second, matching the source-side asymmetry needed after specialization. The induction step uses the bounded-degree polar-derivative root-containment theorem proved in c958eb8. Existing exact-degree callers are recovered with .le. No local build was run; comparator CI remains the validation oracle.

[PerAlexandersson]

Implemented the bounded-degree polarization theorem in commit ff4c824 (PR #301).

mvUpperHalfPlaneStable_reducedPolarization now assumes (binomialLift n f).natDegree ≤ n, and mvUpperHalfPlaneStable_polarization assumes p.natDegree ≤ n. The normalization remains at the ambient cap n. The auxiliary root polynomial retains exact degree n, matching the apolarity proof. A Lean source comment cites Borcea--Brändén, arXiv:0809.0401, Proposition 2.4, and records why the upper half-plane convexity permits bounded degree. Two exact-degree rectangular-polarization callers were weakened with .le. Comparator CI is the validation oracle.