Extend affine finite-symbol sufficiency to degree boxes

[PerAlexandersson]

Summary

Implements the finite degree-box sufficiency direction along the exact
Borcea--Brändén polarization proof.

• packages source polarization Π^up_n and diagonal projection Π^down_n;
• defines the lifted operator Π(T) = T ∘ Π^down_n;
• proves diagonal reconstruction and the full Lemma 2.5 symbol identity;
• transfers symbol stability using Proposition 2.4;
• proves finiteSymbol_finOne_preserves_stability;
• defines the complex-linear bidiagonal operator and its degree-box restriction;
• identifies its genuine algebraic symbol with
  complexifyMv (finiteAlgebraicSymbol d (bidiagonalLinearMap alpha beta));
• proves complexBidiagonalDegreeBox_preserves_stability.

The explicit bidiagonal endpoint assumes genuine affine bivariate-symbol
stability and concludes stable-or-zero output. It does not use or claim the
refuted homogeneous FiniteSymbolPF.finiteSymbol route, the one-sided Jensen
certificate, PF preservation, ASW, real-rootedness, or interlacing.

Primary source: Borcea--Brändén I, Theorem 1.1, Section 2.2, equations
(2.1)--(2.2), Proposition 2.4, and Lemma 2.5.

No local Lake build was run under the active one-shot workflow. Comparator CI
is the validation oracle.

Closes #297.
Refs #238. Required by #240.

[PerAlexandersson]

Source-route step pushed in d6b6b20: polarizationDegreeBox n p packages Π↑ₙ p in degreeOfLE (Fin n) ℂ (fun _ => 1), directly from the proved multiaffineness theorem. This is the domain required by the checked multiaffine finite-symbol theorem; it does not assert a new stability fact.

[PerAlexandersson]

Equation (2.2) source-side reconstruction is now pushed in 12896668. New witnesses: diagonalProjection is the complex-linear map identifying all Fin n variables with the unique univariate variable, and diagonalProjection_polarizationDegreeBox proves Π↓ₙ (Π↑ₙ p) = p for p.natDegree ≤ n. Axle request: 4b35016e-2a0b-4223-81e6-268e50d5dd6d. The remaining degree-box codomain bound is still an explicit proof obligation, not an assumption.

[PerAlexandersson]

Diagonal degree-box bound pushed in 5e8c5058. New reusable witnesses are MvPolynomial.totalDegree_le_sum_degreeOf and MvPolynomial.natDegree_uniqueAlgEquiv_le_totalDegree; the issue-specific theorem natDegree_diagonalProjection_le combines them with totalDegree_rename_le and the degreeOfLE property. Axle requests: 6f0fbf79-f2b0-4b76-924e-821920293ab1 and f99c302f-2eee-4e0f-9edb-961653a716ad. No stability conclusion or preserver assumption is introduced.

[PerAlexandersson]

Degree-box source projection pushed in 003c6bb5. New witnesses: MvPolynomial.degreeOf_uniqueAlgEquiv_symm, diagonalProjectionDegreeBox, and coe_diagonalProjectionDegreeBox_polarizationDegreeBox. The map is built by domRestrict/codRestrict, and proves the source-side reconstruction identity in the actual one-variable degree box. Axle requests: 9062c5fc-93d0-4f7d-bb02-6994b4ea0b54 and 9f348861-2452-4e0d-a5a3-326f19042d9a.

[PerAlexandersson]

Mandatory cleanup pass pushed in 0226016c. natDegree_uniqueAlgEquiv_le_totalDegree no longer repeats coefficient-support reasoning: it now follows from the exact preceding theorem degreeOf_uniqueAlgEquiv_symm and degreeOf_le_totalDegree. Declaration names/statements are unchanged. Axle request: 316fefbe-7138-4397-8a96-3951f2ed5a09.

[PerAlexandersson]

Linear source polarization pushed in 734df989. New witnesses: polarizationLinearMap, polarizationDegreeBoxLinearMap, and diagonalProjectionDegreeBox_comp_polarizationDegreeBoxLinearMap. This proves Π↓ₙ ∘ Π↑ₙ = id on the actual one-variable degree box, with the degree bound derived from the subtype property. Axle requests: 4a2762d0-a8e4-40de-b6e7-17e2e53b26d0 and 47cd1415-d31d-4774-aee4-6fa685e6e392.

[PerAlexandersson]

Source-lifted operator pushed in d9eb16d5. New module: BorceaBranden.Applications.DegreeBoxPolarization. Witnesses: sourcePolarizedOperator n T = T ∘ Π↓ₙ and sourcePolarizedOperator_comp_polarizationDegreeBoxLinearMap, proving (T ∘ Π↓ₙ) ∘ Π↑ₙ = T. Axle request 16fe4add-ef2d-4294-8dd4-d14807efe26a checked the abstract linear-map identity. No symbol-stability claim is made yet.

[PerAlexandersson]

Mandatory cleanup pass pushed in 6fdc02be. The four finite-sum add/smul lemmas used only to construct polarizationLinearMap are now private, leaving the linear map as the sole public linearity API. External-use search found no callers. Unused membership binders and a duplicate simp only step were also removed; theorem behavior is unchanged.

[PerAlexandersson]

Comparator repair 5c8391c is pushed. The only failure was a stuck Unique metavariable in Polarization.lean: the generic degreeOf_uniqueAlgEquiv_symm rewrite now uses an explicit Fin 1 specialization and direct symm_apply_apply normalization. Axle 4.31 request 1719741b-e188-4ba4-bcb2-282701929605 checked the exact elaboration shape. No local Lake build was run; comparator CI is restarting.

[PerAlexandersson]

Continuation 134 also pushes 33d0be6, the first formal coefficient slice of the source-block Lemma 2.5 identity. MvPolynomial.boxChoose_one_of_le_one proves that a multiaffine source basis exponent contributes box coefficient 1, since every coordinate is 0 or 1. Axle 4.31 request 1d708212-5d13-4a12-b2bf-a281450407b0 checked the generic warning-free proof. Next is the diagonalProjectionDegreeBox image of a bounded basis monomial, then grouping by total exponent to recover choose(n,k).

[PerAlexandersson]

Continuation 135 pushes aaee7e3. New theorem diagonalProjection_basisDegreeOfLE proves the exact basis calculation required by the source-side Borcea-Branden Lemma 2.5: collapsing all Fin n variables sends the bounded multiaffine basis monomial m to X ^ m.degree. The private helper isolates rename_monomial, uniqueAlgEquiv_monomial, and the mapDomain collision sum. Axle 4.31 request d76a378d-8881-4e1a-8c1d-ce140ebf091b checked the full generic identity without warnings. No local Lake build was run.

[PerAlexandersson]

Mandatory cleanup continuation 136 pushes b016190. The one-use private uniqueAlgEquiv_rename_const_monomial wrapper is removed, and its already checked mapDomain collision calculation is inlined into diagonalProjection_basisDegreeOfLE. This deletes eight net lines and reduces private API without changing the public theorem, source route, or mathematics. It reuses Axle 4.31 request d76a378d-8881-4e1a-8c1d-ce140ebf091b; no local Lake build was run.

[PerAlexandersson]

Continuation 137 pushes 68cfa13, completing the basis-level source lift required by Borcea-Branden Lemma 2.5.

• diagonalDegreeBoxIndex packages total degree as the canonical bounded Fin 1 exponent.
• diagonalProjectionDegreeBox_basisDegreeOfLE identifies the degree-box diagonal image with that actual basis element.
• sourcePolarizedOperator_basisDegreeOfLE sends the lifted multiaffine basis monomial to T applied to the original degree-n basis monomial of the same total degree.

The sharp degree bound comes directly from m_i <= 1 and card(Fin n) = n. Axle 4.31 requests 94e0037b-2879-4ea8-a26f-898adba5cc5f and d76a378d-8881-4e1a-8c1d-ce140ebf091b checked the supporting constructions. No local Lake build was run; comparator CI is restarting.

[PerAlexandersson]

Continuation 138 pushes ba13770, formalizing the subset reindexing in the source-side Lemma 2.5 calculation.

• degreeOneExponentEquivFinset identifies bounded zero-one Finsupp exponents with finite supports, reusing the existing indicator/support lemmas.
• card_support_eq_degree_of_le_one proves that support cardinality is the total exponent degree.
• sum_degreeOneExponent_eq_sum_finset reindexes the lifted finite-symbol basis sum by subsets of Fin n.

Axle 4.31 requests 6d854db7-8597-45a4-92af-ccda66023c93 and 8491b45a-d6d2-4177-bd1a-834d23836805 checked the generic equivalence/reindex and warning-free cardinality proof. No local Lake build was run. Next is powersetCard grouping to recover choose(n,k).

[PerAlexandersson]

Scheduled cleanup pass: commit 72615fb removes redundant definitional unfolding around the specialized univariate polynomial and consolidates adjacent unfolds in specializeLeft_sourceBlockPolarization (4 insertions, 8 deletions). No theorem statement, definition, hypothesis, normalization, or source reference changed. Comparator CI will validate the combined bridge and cleanup.

[PerAlexandersson]

Commit 717ad29 adds the general specialization degree lemma needed to combine specializeLeft_sourceBlockPolarization with bounded polarization stability. It proves the full natDegree ≤ source degreeOf statement via optionEquivLeft and Polynomial.natDegree_map_le, with no additional analytic assumption. Comparator CI is the validation oracle.

[PerAlexandersson]

Comparator for 717ad29 found a single explicit-argument mismatch in MvPolynomial.optionEquivLeft_elim_eval. Commit 096a3f3 supplies this Mathlib version’s required ℂ and τ arguments. The theorem statement and optionEquivLeft/natDegree_map_le proof route are unchanged. The full source-block stability-transfer theorem has been outlined but was intentionally not added on top of the failing prerequisite.

[PerAlexandersson]

Scheduled cleanup pass: commit 52e4093 folds the local Q reduction into the existing simplifier and replaces the final degree calc chain with rewrites by hpoly/hQdeg followed by Polynomial.natDegree_map_le (3 insertions, 11 deletions). Both explicit imports remain because they own declarations used by the proof. No statement or mathematical route changed.

[PerAlexandersson]

Commit 8e60f2e assembles the source-block stability-transfer theorem from the three proved prerequisites. It follows Borcea--Brändén Proposition 2.4 fiberwise and retains ambient cap n. The preceding comparator rebuild was still running after eight minutes without a new failure; the new head comparator will validate the combined prerequisite and transfer theorem.

[PerAlexandersson]

Commit 5b7fd6a proves the arbitrary degree-box source bound for algebraicSymbol, directly from the complementary-monomial expansion in Borcea--Brändén §1.1. The existing all-ones proof is intentionally left unchanged until continuation 201, the scheduled cleanup pass, where it can be deduplicated after comparator feedback.

[PerAlexandersson]

Scheduled cleanup pass: commit 9b5367f replaces the duplicated 59-line proof of degreeOf_algebraicSymbol_one_inr_le with a direct application of degreeOf_algebraicSymbol_inr_le, and removes one unused membership binder (2 insertions, 58 deletions). No theorem statement, definition, or mathematical route changed.

[PerAlexandersson]

Commit f9e539f assembles the degree-box finite-symbol stability implication as a proved theorem from the full Lemma 2.5 identity, the general source-degree bound, and Proposition 2.4. This isolates the remaining work correctly: the Jensen certificate still needs a sourced proof of genuine affine-symbol stability rather than being treated as equivalent to a real nonnegative pencil condition.

[PerAlexandersson]

Commit fe13bc2 records the source-audited Jensen obstruction at jensenPencilBidiagonalPreserverStatement. This prevents the now-proved degree-box finite-symbol machinery from being misapplied to the weaker real λ ≥ 0 pencil certificate. The comment cites Borcea--Brändén Theorem 1.1, Garloff--Wagner Theorem 12(b), and issue #240’s exact degree-two counterexample.

[PerAlexandersson]

Scheduled cleanup pass: commit 643e4aa moves the displaced “Termwise form” docstring back onto rename_algebraicSymbol_sourcePolarizedOperator_eq_sum, merges the Jensen obstruction into the backend proposition’s own docstring, and golfs the finite-symbol stability transfer to one simpa. No declaration, hypothesis, source reference, or mathematical warning changed.

[PerAlexandersson]

Commit f18c2fe extends the backend documentation with the exact unmatched hypotheses from Brändén’s PF-specific Theorem 3.6 (arXiv:math/0403364, paper-cache record 91). This closes another tempting but invalid proof route without changing any API.

[PerAlexandersson]

Pushed 647cf8a8 to repair the comparator failures in DegreeBoxPolarization.lean. This does not change the Borcea--Branden Proposition 2.4 / Lemma 2.5 definitions or theorem statements: it imports the module owning the coordinatewise source-degree bound, uses Polynomial ℂ instead of unsupported ℂ[X] notation, and follows the existing explicit map_add/map_mul induction pattern to avoid the aeval/bind₁ mismatch. No local Lake build was run; fresh CI will validate the repair.

[PerAlexandersson]

Pushed f8d2c818 for the two remaining comparator goals. Both are explicit homomorphism identities for MvPolynomial.C: additivity is closed by map_add, and the mul_X case by map_mul after exposing function composition. No theorem statement, polarization definition, or Borcea--Branden normalization changed. No local Lake build was run; fresh comparator CI is authoritative.