Extend affine finite-symbol sufficiency to degree-d source boxes

[PerAlexandersson]

Context

Merged theorem RealRooted.BorceaBranden.finiteSymbol_preserves_stability is
the genuine affine Borcea--Branden finite-symbol implication, but its source is
restricted to the multiaffine box MvPolynomial.degreeOfLE sigma C (fun _ => 1).

Issue #240 needs the exact symbol computed by
finiteAlgebraicSymbol_bidiagonalLinearMap, whose source is a one-variable
degree-d box. These theorem shapes do not compose directly.

Primary source: Borcea--Branden, arXiv:0809.0401, Proposition 2.4, equation
(2.2), and Lemma 2.5. Paper-cache id: 84.

Required outline

1. Polarize each source coordinate of degree kappa i into a block of kappa i
   multiaffine variables, tracking binomial normalization exactly.
2. Define the lifted linear operator on the multiaffine source box and prove
   diagonal specialization reconstructs the original operator value.
3. Prove the algebraic symbol of the lifted operator is the corresponding
   source-block polarization of the genuine affine algebraic symbol.
4. Transfer stability of the original symbol to the lifted multiaffine symbol
   using the checked polarization/Grace--Walsh--Szego API.
5. Apply checked theorem finiteSymbol_preserves_stability.
6. Specialize back to obtain the zero-aware stability conclusion for the
   original degree-box operator.

For the first application, it is enough to handle sigma = Fin 1 with degree
bound d; a general coordinatewise-degree theorem is preferable only if it does
not obscure the normalization.

Acceptance criteria

• Add a checked theorem, not a def-Statement proposition, sorry, axiom, or an
  assumption of the desired preserver conclusion.
• The conclusion must remain zero-aware.
• Prove the exact algebraic-symbol/polarization identity, including all
  binomial coefficients and variable renamings.
• Do not use the refuted homogeneous FiniteSymbolPF.finiteSymbol route.
• Demonstrate the application to finiteAlgebraicSymbol_bidiagonalLinearMap
  without claiming that the current one-sided Jensen certificate implies
  affine-symbol stability.
• Run focused and aggregate Lake builds and report the theorem witness names.

Parent: #238. Required by: #240.

[PerAlexandersson]

Paper-cache record 84 confirms the exact Borcea--Branden composition on printed pp. 10--12.

For the Fin 1 degree-d source box, polarization must send

z^k |-> binom(d,k)^(-1) E_k(z_1,...,z_d).

The lifted operator is Pi(T) = PiUp_gamma o T o PiDown_d; reconstruction is equation (2.2), T = PiDown_gamma o Pi(T) o PiUp_d. Lemma 2.5 gives the exact affine-symbol identity

G_(Pi(T)) = PiUp_(gamma+d)(G_T),

with separate polarization blocks for output variables and source-symbol variables. Proposition 2.4 transfers stability to that symbol, the merged multiaffine finiteSymbol_preserves_stability applies to Pi(T), and diagonal reconstruction returns the original zero-aware conclusion.

This fixes the implementation order and normalization before Lean work begins. It does not use the homogeneous FiniteSymbolPF.finiteSymbol route and makes no claim that issue #240's current one-sided Jensen certificate implies affine-symbol stability.

[PerAlexandersson]

First checked implementation slice is pushed in db5d5be4 on draft PR #298.

New theorem rename_polarization_const upgrades the existing pointwise diagonal specialization to the polynomial identity

MvPolynomial.rename (fun _ : Fin n => (0 : Fin 1)) (polarization n p) =
  (MvPolynomial.uniqueAlgEquiv ℂ (Fin 1)).symm p

under p.natDegree <= n. This is the source reconstruction component of equation (2.2); it uses no homogeneous finite symbol and makes no Jensen-certificate claim. Axle 4.31 request: d7f34772-aaab-499d-bf64-05b536b4e045. Next is packaging polarization into the all-ones degree box and defining the lifted operator.

[PerAlexandersson]

Source/API audit update: Lemma 2.5 source diagonal identity is now proved on PR #301. For Proposition 2.4, the current checked mvUpperHalfPlaneStable_polarization theorem is exact-degree only because grace_apolarity_lowerHalf and its polar-derivative induction require degree n. The next sound theorem is the convex upper-half-plane Grace--Walsh--Szegő coincidence statement (or its specialization to polarization n p), from which the degree-at-most stability transfer follows using eval_polarization_const. Commit 554e81a adds the required checked symmetry lemmas; no analytic implication is assumed.

[PerAlexandersson]

GWS source-route update: Borcea--Brändén Part II proves the cited convex coincidence theorem by stability of partial transposition averages, convergence to full symmetrization via Hurwitz, and uniqueness from diagonal restriction. Commit c4b2609 adds the checked algebraic full-symmetrization core and diagonal-evaluation preservation. The current exact-degree apolarity theorem cannot simply be weakened; no such assumption was added.

[PerAlexandersson]

Source-driven Part II progress: commit 1278c753 on PR #301 adds im_bivariateQuotient_eq_bivariateV1_div_normSq and im_bivariateQuotient_eq_bivariateV2_div_normSq, the two exact real-boundary identities used in Lemma 1.4. The cached source confirms Lemma 1.4 assumes d ≠ 0; no d = 0 extension or minimum-principle implication was guessed. Axle 4.31 checked both algebraic proofs in request 382adb3a-2332-42d6-a0f6-fb09389894dc.

[PerAlexandersson]

Commit b6a37901 on PR #301 adds the next exact Part II, Lemma 1.4 slice: add_mul_real_ne_zero_of_im_div_pos, im_bivariateQuotient_pos_iff_bivariateV1_pos, and im_bivariateQuotient_pos_iff_bivariateV2_pos. These turn the checked boundary identities into positivity equivalences using denominator nonvanishing and positive normSq; the harmonic minimum-principle step remains explicit and unproved. Axle 4.31 request: a10ec869-6bfe-4e98-a3a6-17185f02917b.

[PerAlexandersson]

Scheduled cleanup commit 6a3b329a on PR #301 deduplicates the symmetric bivariate proofs. The V2 boundary quotient, positivity bridge, and partial-symmetrization theorems are now direct instances of their V1 counterparts under b ↔ c; public statements are unchanged. Axle 4.31 request: e490272f-6e1d-4435-8bff-4d4c154d53c6.

[PerAlexandersson]

Commit 8dba4c67 on PR #301 formalizes the next Part II, Lemma 1.4 source step: add_mul_ne_zero_of_im_div_pos handles every z in the closed upper half-plane, while bivariate_eq_factor_quotient and bivariate_eq_zero_iff implement the exact solve-for-w factorization preceding equation (1.2). The real-boundary denominator theorem is now a corollary. No minimum-principle or stability equivalence is assumed. Axle 4.31 request: 9243ab43-52d9-4812-b426-1696674f700b.

[PerAlexandersson]

Commit c3d8a0b1 on PR #301 adds bivariate_ne_zero_of_quotient_im_pos and bivariate_ne_zero_of_im_div_pos_of_quotient_im_pos. These use the checked unique-zero formula to prove the purely algebraic direction from positive solved-quotient imaginary part to bivariate nonvanishing in the upper half-plane. The MvPolynomial encoding bridge and the analytic converse/open-mapping/minimum-principle steps remain explicit. Axle 4.31 request: 709c30c2-38eb-413c-82a5-bf4d6045126b.

[PerAlexandersson]

Scheduled cleanup commit 24ed20ac on PR #301 removes the duplicated bivariateV2 quadratic formula: it is now defined as bivariateV1 a c b d x, making the source’s b ↔ c symmetry explicit while preserving the public API. Axle 4.31 checked all affected quotient, positivity, and partial-symmetrization theorems (a1cb96b6-a89b-4fce-adc2-99530f656078).

[PerAlexandersson]

Commit b08fdf10 on PR #301 adds the first repository-level bridge for Part II equation (1.2): bivariateMultiaffinePolynomial, eval_bivariateMultiaffinePolynomial, and mvUpperHalfPlaneStable_bivariate_of_quotient_im_pos. A focused search found no existing four-coefficient constructor. The theorem proves only the checked quotient-positivity-to-MvUpperHalfPlaneStable direction; the analytic converse remains explicit. Axle 4.31 request: 3f1e5067-7555-4ff6-ac46-691cf8b40540.

[PerAlexandersson]

Commit 68bfea4c on PR #301 adds quotient_im_nonneg_of_mvUpperHalfPlaneStable_bivariate: stability forces the solved quotient into the closed upper half-plane by substituting its unique root. The API audit found no ready harmonic minimum principle; strict positivity still requires an open-mapping/nonconstant-map step, and the real-boundary converse requires a separate derived harmonic argument. Axle 4.31 request: bc007f07-d240-4fdc-9958-1255e7325394.

[PerAlexandersson]

Scheduled cleanup commit 33979985 on PR #301 golfs quotient_im_nonneg_of_mvUpperHalfPlaneStable_bivariate: the two Fin 2 coordinate branches are handled uniformly and the final contradiction is direct. Statement and mathematical route unchanged. Axle 4.31 request: 79c485a5-0eb2-4dd3-bc30-9f886c009de3.