From db5d5be4d13dcf0b064b44006f1787bb0c6f9b59 Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Mon, 3 Aug 2026 08:02:35 +0000 Subject: [PATCH 01/81] feat: prove polarization diagonal reconstruction --- RealRooted/Polarization.lean | 21 +++++++++++++++++++++ 1 file changed, 21 insertions(+) diff --git a/RealRooted/Polarization.lean b/RealRooted/Polarization.lean index 650b35f10..d71f5e991 100644 --- a/RealRooted/Polarization.lean +++ b/RealRooted/Polarization.lean @@ -1,3 +1,4 @@ +import Mathlib.Algebra.MvPolynomial.Equiv import Mathlib.RingTheory.Polynomial.Vieta import RealRooted.GraceHalfPlane import RealRooted.Multiaffine @@ -116,6 +117,26 @@ theorem eval_polarization_const {n : ℕ} {p : ℂ[X]} (hp : p.natDegree ≤ n) unfold polarization rw [eval_reducedPolarization_const, binomialLift_binomialUnlift hp] +/-- Renaming every polarization variable to the unique variable reconstructs +the original univariate polynomial. This is the diagonal identity for +polarization. -/ +theorem rename_polarization_const {n : ℕ} {p : ℂ[X]} + (hp : p.natDegree ≤ n) : + MvPolynomial.rename (fun _ : Fin n ↦ (0 : Fin 1)) (polarization n p) = + (MvPolynomial.uniqueAlgEquiv ℂ (Fin 1)).symm p := by + apply (MvPolynomial.uniqueAlgEquiv ℂ (Fin 1)).injective + rw [AlgEquiv.apply_symm_apply] + apply Polynomial.funext + intro w + change Polynomial.eval₂ (RingHom.id ℂ) w + ((MvPolynomial.uniqueAlgEquiv ℂ (Fin 1)) + (MvPolynomial.rename (fun _ : Fin n ↦ (0 : Fin 1)) + (polarization n p))) = p.eval w + rw [MvPolynomial.eval₂_const_uniqueAlgEquiv] + rw [MvPolynomial.eval₂_rename] + change MvPolynomial.eval (fun _ : Fin n ↦ w) (polarization n p) = p.eval w + exact eval_polarization_const hp w + /-- Evaluation of a polarization in elementary symmetric functions. -/ theorem eval_polarization (n : ℕ) (p : ℂ[X]) (z : Fin n → ℂ) : MvPolynomial.eval z (polarization n p) = From d6b6b20cd2f520de7b58839ee98b3a5ef9105f7a Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Mon, 3 Aug 2026 08:09:05 +0000 Subject: [PATCH 02/81] Package polarization in degree box --- RealRooted/Polarization.lean | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/RealRooted/Polarization.lean b/RealRooted/Polarization.lean index d71f5e991..65b493aae 100644 --- a/RealRooted/Polarization.lean +++ b/RealRooted/Polarization.lean @@ -1,4 +1,5 @@ import Mathlib.Algebra.MvPolynomial.Equiv +import RealRooted.Mathlib.Algebra.MvPolynomial.Stability.DegreeBox import Mathlib.RingTheory.Polynomial.Vieta import RealRooted.GraceHalfPlane import RealRooted.Multiaffine @@ -137,6 +138,18 @@ theorem rename_polarization_const {n : ℕ} {p : ℂ[X]} change MvPolynomial.eval (fun _ : Fin n ↦ w) (polarization n p) = p.eval w exact eval_polarization_const hp w +/-- Package polarization as the multiaffine source polynomial +`Π↑ₙ p` in the all-ones degree box. -/ +noncomputable def polarizationDegreeBox (n : ℕ) (p : ℂ[X]) : + MvPolynomial.degreeOfLE (Fin n) ℂ (fun _ => 1) := + ⟨polarization n p, + (MvPolynomial.mem_degreeOfLE_iff_degreeOf (polarization n p)).2 + (isMultiaffine_polarization n p)⟩ + +@[simp] +theorem coe_polarizationDegreeBox (n : ℕ) (p : ℂ[X]) : + (polarizationDegreeBox n p : MvPolynomial (Fin n) ℂ) = polarization n p := rfl + /-- Evaluation of a polarization in elementary symmetric functions. -/ theorem eval_polarization (n : ℕ) (p : ℂ[X]) (z : Fin n → ℂ) : MvPolynomial.eval z (polarization n p) = From 12896668616c7078d826a717f80732d1d19a45ec Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Mon, 3 Aug 2026 08:11:45 +0000 Subject: [PATCH 03/81] Define diagonal polarization projection --- RealRooted/Polarization.lean | 21 +++++++++++++++++++++ 1 file changed, 21 insertions(+) diff --git a/RealRooted/Polarization.lean b/RealRooted/Polarization.lean index 65b493aae..13130699d 100644 --- a/RealRooted/Polarization.lean +++ b/RealRooted/Polarization.lean @@ -150,6 +150,27 @@ noncomputable def polarizationDegreeBox (n : ℕ) (p : ℂ[X]) : theorem coe_polarizationDegreeBox (n : ℕ) (p : ℂ[X]) : (polarizationDegreeBox n p : MvPolynomial (Fin n) ℂ) = polarization n p := rfl +/-- The diagonal projection `Π↓ₙ`, obtained by identifying every polarization +variable with the unique univariate variable. -/ +noncomputable def diagonalProjection (n : ℕ) : + MvPolynomial (Fin n) ℂ →ₗ[ℂ] ℂ[X] where + toFun q := + MvPolynomial.uniqueAlgEquiv ℂ (Fin 1) + (MvPolynomial.rename (fun _ : Fin n => (0 : Fin 1)) q) + map_add' q r := by simp + map_smul' c q := by + simp [MvPolynomial.smul_eq_C_mul, Polynomial.smul_eq_C_mul] + +/-- Equation (2.2) on the source side: diagonal projection is a left inverse +to polarization on polynomials of degree at most `n`. -/ +theorem diagonalProjection_polarizationDegreeBox {n : ℕ} {p : ℂ[X]} + (hp : p.natDegree ≤ n) : + diagonalProjection n (polarizationDegreeBox n p) = p := by + change MvPolynomial.uniqueAlgEquiv ℂ (Fin 1) + (MvPolynomial.rename (fun _ : Fin n => (0 : Fin 1)) (polarization n p)) = p + rw [rename_polarization_const hp] + exact (MvPolynomial.uniqueAlgEquiv ℂ (Fin 1)).apply_symm_apply p + /-- Evaluation of a polarization in elementary symmetric functions. -/ theorem eval_polarization (n : ℕ) (p : ℂ[X]) (z : Fin n → ℂ) : MvPolynomial.eval z (polarization n p) = From 5e8c5058f6ca0c2718fdcc628db7d1a340c244eb Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Mon, 3 Aug 2026 08:21:45 +0000 Subject: [PATCH 04/81] Bound degree of diagonal projection --- .../Mathlib/Algebra/MvPolynomial/Degrees.lean | 30 +++++++++++++++++++ .../Mathlib/Algebra/MvPolynomial/Equiv.lean | 27 +++++++++++++++++ RealRooted/Polarization.lean | 20 ++++++++++++- 3 files changed, 76 insertions(+), 1 deletion(-) create mode 100644 RealRooted/Mathlib/Algebra/MvPolynomial/Degrees.lean create mode 100644 RealRooted/Mathlib/Algebra/MvPolynomial/Equiv.lean diff --git a/RealRooted/Mathlib/Algebra/MvPolynomial/Degrees.lean b/RealRooted/Mathlib/Algebra/MvPolynomial/Degrees.lean new file mode 100644 index 000000000..b40bcf548 --- /dev/null +++ b/RealRooted/Mathlib/Algebra/MvPolynomial/Degrees.lean @@ -0,0 +1,30 @@ +import Mathlib.Algebra.MvPolynomial.Degrees + +/-! +# Additional total-degree bounds + +This file contains Mathlib-shaped compatibility lemmas for multivariate +polynomial degrees. +-/ + +open scoped BigOperators + +namespace MvPolynomial + +/-- Total degree is at most the sum of the coordinatewise degrees. -/ +theorem totalDegree_le_sum_degreeOf {σ R : Type*} [Fintype σ] [CommSemiring R] + (p : MvPolynomial σ R) : + p.totalDegree ≤ ∑ i, p.degreeOf i := by + classical + rw [totalDegree] + apply Finset.sup_le + intro d hd + calc + d.sum (fun _ e => e) = ∑ i, d i := by + rw [Finsupp.sum_fintype] + intro + rfl + _ ≤ ∑ i, p.degreeOf i := + Finset.sum_le_sum fun i _ => le_degreeOf_of_mem_support i hd + +end MvPolynomial diff --git a/RealRooted/Mathlib/Algebra/MvPolynomial/Equiv.lean b/RealRooted/Mathlib/Algebra/MvPolynomial/Equiv.lean new file mode 100644 index 000000000..c5bd8ea26 --- /dev/null +++ b/RealRooted/Mathlib/Algebra/MvPolynomial/Equiv.lean @@ -0,0 +1,27 @@ +import Mathlib.Algebra.MvPolynomial.Equiv +import Mathlib.Algebra.Polynomial.Degree.Lemmas + +/-! +# Degree bounds for univariate multivariate-polynomial equivalences + +This file contains Mathlib-shaped compatibility lemmas for +`MvPolynomial.uniqueAlgEquiv`. +-/ + +namespace MvPolynomial + +/-- Passing from a uniquely indexed multivariate polynomial to a univariate +polynomial does not increase total degree. -/ +theorem natDegree_uniqueAlgEquiv_le_totalDegree + {σ R : Type*} [Unique σ] [CommSemiring R] (p : MvPolynomial σ R) : + (MvPolynomial.uniqueAlgEquiv R σ p).natDegree ≤ p.totalDegree := by + rw [Polynomial.natDegree_le_iff_coeff_eq_zero] + intro n hn + rw [MvPolynomial.coeff_uniqueAlgEquiv] + by_contra hcoeff + have hsupp : Finsupp.single default n ∈ p.support := + MvPolynomial.mem_support_iff.mpr hcoeff + have hle := MvPolynomial.le_totalDegree hsupp + exact (not_le_of_gt hn) (by simpa using hle) + +end MvPolynomial diff --git a/RealRooted/Polarization.lean b/RealRooted/Polarization.lean index 13130699d..cce153b0f 100644 --- a/RealRooted/Polarization.lean +++ b/RealRooted/Polarization.lean @@ -1,4 +1,5 @@ -import Mathlib.Algebra.MvPolynomial.Equiv +import RealRooted.Mathlib.Algebra.MvPolynomial.Degrees +import RealRooted.Mathlib.Algebra.MvPolynomial.Equiv import RealRooted.Mathlib.Algebra.MvPolynomial.Stability.DegreeBox import Mathlib.RingTheory.Polynomial.Vieta import RealRooted.GraceHalfPlane @@ -161,6 +162,23 @@ noncomputable def diagonalProjection (n : ℕ) : map_smul' c q := by simp [MvPolynomial.smul_eq_C_mul, Polynomial.smul_eq_C_mul] +/-- Diagonal projection of an all-ones degree-box polynomial has degree at +most the size of its polarization block. -/ +theorem natDegree_diagonalProjection_le {n : ℕ} + (q : MvPolynomial.degreeOfLE (Fin n) ℂ (fun _ => 1)) : + (diagonalProjection n q).natDegree ≤ n := by + have hdeg : ∀ i, q.1.degreeOf i ≤ 1 := + (MvPolynomial.mem_degreeOfLE_iff_degreeOf q.1).mp q.2 + change (MvPolynomial.uniqueAlgEquiv ℂ (Fin 1) + (MvPolynomial.rename (fun _ : Fin n => (0 : Fin 1)) q.1)).natDegree ≤ n + calc + _ ≤ (MvPolynomial.rename (fun _ : Fin n => (0 : Fin 1)) q.1).totalDegree := + MvPolynomial.natDegree_uniqueAlgEquiv_le_totalDegree _ + _ ≤ q.1.totalDegree := MvPolynomial.totalDegree_rename_le _ _ + _ ≤ ∑ i, q.1.degreeOf i := MvPolynomial.totalDegree_le_sum_degreeOf q.1 + _ ≤ ∑ _ : Fin n, 1 := Finset.sum_le_sum fun i _ => hdeg i + _ = n := by simp + /-- Equation (2.2) on the source side: diagonal projection is a left inverse to polarization on polynomials of degree at most `n`. -/ theorem diagonalProjection_polarizationDegreeBox {n : ℕ} {p : ℂ[X]} From 003c6bb530b3a76de9501ad2a710706a58bc68ec Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Mon, 3 Aug 2026 08:26:15 +0000 Subject: [PATCH 05/81] Restrict diagonal projection to degree boxes --- .../Mathlib/Algebra/MvPolynomial/Equiv.lean | 25 +++++++++++++++ RealRooted/Polarization.lean | 31 +++++++++++++++++++ 2 files changed, 56 insertions(+) diff --git a/RealRooted/Mathlib/Algebra/MvPolynomial/Equiv.lean b/RealRooted/Mathlib/Algebra/MvPolynomial/Equiv.lean index c5bd8ea26..2b840343e 100644 --- a/RealRooted/Mathlib/Algebra/MvPolynomial/Equiv.lean +++ b/RealRooted/Mathlib/Algebra/MvPolynomial/Equiv.lean @@ -24,4 +24,29 @@ theorem natDegree_uniqueAlgEquiv_le_totalDegree have hle := MvPolynomial.le_totalDegree hsupp exact (not_le_of_gt hn) (by simpa using hle) +/-- The degree in the unique variable after converting a univariate polynomial +to an `MvPolynomial` is its natural degree. -/ +theorem degreeOf_uniqueAlgEquiv_symm + {σ R : Type*} [Unique σ] [CommSemiring R] (p : Polynomial R) : + degreeOf default ((MvPolynomial.uniqueAlgEquiv R σ).symm p) = + p.natDegree := by + apply le_antisymm + · rw [degreeOf_le_iff] + intro d hd + have hcoeff : p.coeff (d default) ≠ 0 := by + rw [← MvPolynomial.coeff_uniqueAlgEquiv_symm R p d] + exact MvPolynomial.mem_support_iff.mp hd + exact Polynomial.le_natDegree_of_ne_zero hcoeff + · rw [Polynomial.natDegree_le_iff_coeff_eq_zero] + intro n hn + have hnotmem : + Finsupp.single default n ∉ + ((MvPolynomial.uniqueAlgEquiv R σ).symm p).support := by + apply MvPolynomial.notMem_support_of_degreeOf_lt default + simpa using hn + have hzero := MvPolynomial.notMem_support_iff.mp hnotmem + rw [MvPolynomial.coeff_uniqueAlgEquiv_symm R p + (Finsupp.single default n)] at hzero + simpa using hzero + end MvPolynomial diff --git a/RealRooted/Polarization.lean b/RealRooted/Polarization.lean index cce153b0f..c1806090e 100644 --- a/RealRooted/Polarization.lean +++ b/RealRooted/Polarization.lean @@ -179,6 +179,25 @@ theorem natDegree_diagonalProjection_le {n : ℕ} _ ≤ ∑ _ : Fin n, 1 := Finset.sum_le_sum fun i _ => hdeg i _ = n := by simp +/-- Diagonal projection as a linear map from the multiaffine source box to the +original one-variable degree box. This is the source-side map `Π↓ₙ`. -/ +noncomputable def diagonalProjectionDegreeBox (n : ℕ) : + MvPolynomial.degreeOfLE (Fin n) ℂ (fun _ => 1) →ₗ[ℂ] + MvPolynomial.degreeOfLE (Fin 1) ℂ (fun _ => n) := + LinearMap.codRestrict (MvPolynomial.degreeOfLE (Fin 1) ℂ (fun _ => n)) + (((MvPolynomial.uniqueAlgEquiv ℂ (Fin 1)).symm.toLinearMap.comp + (diagonalProjection n)).domRestrict + (MvPolynomial.degreeOfLE (Fin n) ℂ (fun _ => 1))) + (fun q => by + apply (MvPolynomial.mem_degreeOfLE_iff_degreeOf _).2 + intro i + change MvPolynomial.degreeOf i + ((MvPolynomial.uniqueAlgEquiv ℂ (Fin 1)).symm + (diagonalProjection n q)) ≤ n + rw [Unique.eq_default i, + MvPolynomial.degreeOf_uniqueAlgEquiv_symm] + exact natDegree_diagonalProjection_le q) + /-- Equation (2.2) on the source side: diagonal projection is a left inverse to polarization on polynomials of degree at most `n`. -/ theorem diagonalProjection_polarizationDegreeBox {n : ℕ} {p : ℂ[X]} @@ -189,6 +208,18 @@ theorem diagonalProjection_polarizationDegreeBox {n : ℕ} {p : ℂ[X]} rw [rename_polarization_const hp] exact (MvPolynomial.uniqueAlgEquiv ℂ (Fin 1)).apply_symm_apply p +/-- Degree-box form of the source reconstruction identity +`Π↓ₙ (Π↑ₙ p) = p`. -/ +theorem coe_diagonalProjectionDegreeBox_polarizationDegreeBox + {n : ℕ} {p : ℂ[X]} (hp : p.natDegree ≤ n) : + (diagonalProjectionDegreeBox n (polarizationDegreeBox n p) : + MvPolynomial (Fin 1) ℂ) = + (MvPolynomial.uniqueAlgEquiv ℂ (Fin 1)).symm p := by + change (MvPolynomial.uniqueAlgEquiv ℂ (Fin 1)).symm + (diagonalProjection n (polarizationDegreeBox n p)) = + (MvPolynomial.uniqueAlgEquiv ℂ (Fin 1)).symm p + rw [diagonalProjection_polarizationDegreeBox hp] + /-- Evaluation of a polarization in elementary symmetric functions. -/ theorem eval_polarization (n : ℕ) (p : ℂ[X]) (z : Fin n → ℂ) : MvPolynomial.eval z (polarization n p) = From 0226016c790035141857e80a3aa27b0d03eb2133 Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Mon, 3 Aug 2026 08:29:05 +0000 Subject: [PATCH 06/81] Deduplicate unique equivalence degree proof --- .../Mathlib/Algebra/MvPolynomial/Equiv.lean | 29 ++++++++++--------- 1 file changed, 15 insertions(+), 14 deletions(-) diff --git a/RealRooted/Mathlib/Algebra/MvPolynomial/Equiv.lean b/RealRooted/Mathlib/Algebra/MvPolynomial/Equiv.lean index 2b840343e..bcfae2931 100644 --- a/RealRooted/Mathlib/Algebra/MvPolynomial/Equiv.lean +++ b/RealRooted/Mathlib/Algebra/MvPolynomial/Equiv.lean @@ -10,20 +10,6 @@ This file contains Mathlib-shaped compatibility lemmas for namespace MvPolynomial -/-- Passing from a uniquely indexed multivariate polynomial to a univariate -polynomial does not increase total degree. -/ -theorem natDegree_uniqueAlgEquiv_le_totalDegree - {σ R : Type*} [Unique σ] [CommSemiring R] (p : MvPolynomial σ R) : - (MvPolynomial.uniqueAlgEquiv R σ p).natDegree ≤ p.totalDegree := by - rw [Polynomial.natDegree_le_iff_coeff_eq_zero] - intro n hn - rw [MvPolynomial.coeff_uniqueAlgEquiv] - by_contra hcoeff - have hsupp : Finsupp.single default n ∈ p.support := - MvPolynomial.mem_support_iff.mpr hcoeff - have hle := MvPolynomial.le_totalDegree hsupp - exact (not_le_of_gt hn) (by simpa using hle) - /-- The degree in the unique variable after converting a univariate polynomial to an `MvPolynomial` is its natural degree. -/ theorem degreeOf_uniqueAlgEquiv_symm @@ -49,4 +35,19 @@ theorem degreeOf_uniqueAlgEquiv_symm (Finsupp.single default n)] at hzero simpa using hzero +/-- Passing from a uniquely indexed multivariate polynomial to a univariate +polynomial does not increase total degree. -/ +theorem natDegree_uniqueAlgEquiv_le_totalDegree + {σ R : Type*} [Unique σ] [CommSemiring R] (p : MvPolynomial σ R) : + (MvPolynomial.uniqueAlgEquiv R σ p).natDegree ≤ p.totalDegree := by + calc + (MvPolynomial.uniqueAlgEquiv R σ p).natDegree = + degreeOf default + ((MvPolynomial.uniqueAlgEquiv R σ).symm + (MvPolynomial.uniqueAlgEquiv R σ p)) := + (degreeOf_uniqueAlgEquiv_symm + (MvPolynomial.uniqueAlgEquiv R σ p)).symm + _ = degreeOf default p := by rw [AlgEquiv.symm_apply_apply] + _ ≤ p.totalDegree := degreeOf_le_totalDegree p default + end MvPolynomial From 734df9895f8ac818b907b86d89f6020cc51e6929 Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Mon, 3 Aug 2026 08:37:35 +0000 Subject: [PATCH 07/81] Define linear source polarization map --- RealRooted/Polarization.lean | 94 ++++++++++++++++++++++++++++++++++++ 1 file changed, 94 insertions(+) diff --git a/RealRooted/Polarization.lean b/RealRooted/Polarization.lean index c1806090e..cad839438 100644 --- a/RealRooted/Polarization.lean +++ b/RealRooted/Polarization.lean @@ -59,6 +59,59 @@ elementary symmetric polynomial is `p.coeff k / choose n k`. -/ def polarization (n : ℕ) (p : ℂ[X]) : MvPolynomial (Fin n) ℂ := reducedPolarization n (binomialUnlift n p) +theorem binomialUnlift_add (n : ℕ) (p q : ℂ[X]) : + binomialUnlift n (p + q) = + binomialUnlift n p + binomialUnlift n q := by + unfold binomialUnlift + rw [← Finset.sum_add_distrib] + apply Finset.sum_congr rfl + intro k hk + rw [Polynomial.coeff_add, add_div, map_add] + +theorem binomialUnlift_smul (n : ℕ) (c : ℂ) (p : ℂ[X]) : + binomialUnlift n (c • p) = c • binomialUnlift n p := by + unfold binomialUnlift + rw [Finset.smul_sum] + apply Finset.sum_congr rfl + intro k hk + simp only [Polynomial.coeff_smul] + simp only [div_eq_mul_inv] + change (Polynomial.monomial k) + (c * p.coeff k * (n.choose k : ℂ)⁻¹) = + c • (Polynomial.monomial k) + (p.coeff k * (n.choose k : ℂ)⁻¹) + rw [mul_assoc] + exact (Polynomial.smul_monomial c k + (p.coeff k * (n.choose k : ℂ)⁻¹)).symm + +theorem reducedPolarization_add (n : ℕ) (p q : ℂ[X]) : + reducedPolarization n (p + q) = + reducedPolarization n p + reducedPolarization n q := by + unfold reducedPolarization + rw [← Finset.sum_add_distrib] + apply Finset.sum_congr rfl + intro k hk + simp [add_mul] + +theorem reducedPolarization_smul (n : ℕ) (c : ℂ) (p : ℂ[X]) : + reducedPolarization n (c • p) = c • reducedPolarization n p := by + unfold reducedPolarization + rw [Finset.smul_sum] + apply Finset.sum_congr rfl + intro k hk + simp [MvPolynomial.smul_eq_C_mul, mul_assoc] + +/-- Polarization as a complex-linear map on univariate polynomials. -/ +noncomputable def polarizationLinearMap (n : ℕ) : + ℂ[X] →ₗ[ℂ] MvPolynomial (Fin n) ℂ where + toFun := polarization n + map_add' p q := by + change polarization n (p + q) = polarization n p + polarization n q + simp only [polarization, binomialUnlift_add, reducedPolarization_add] + map_smul' c p := by + change polarization n (c • p) = c • polarization n p + simp only [polarization, binomialUnlift_smul, reducedPolarization_smul] + theorem isMultiaffine_reducedPolarization (n : ℕ) (p : ℂ[X]) : MvPolynomial.IsMultiaffine (reducedPolarization n p) := by unfold reducedPolarization @@ -151,6 +204,20 @@ noncomputable def polarizationDegreeBox (n : ℕ) (p : ℂ[X]) : theorem coe_polarizationDegreeBox (n : ℕ) (p : ℂ[X]) : (polarizationDegreeBox n p : MvPolynomial (Fin n) ℂ) = polarization n p := rfl +/-- Source polarization `Π↑ₙ` as a linear map from the one-variable degree-`n` +box to the multiaffine all-ones box. -/ +noncomputable def polarizationDegreeBoxLinearMap (n : ℕ) : + MvPolynomial.degreeOfLE (Fin 1) ℂ (fun _ => n) →ₗ[ℂ] + MvPolynomial.degreeOfLE (Fin n) ℂ (fun _ => 1) := + LinearMap.codRestrict (MvPolynomial.degreeOfLE (Fin n) ℂ (fun _ => 1)) + ((polarizationLinearMap n).comp + ((MvPolynomial.uniqueAlgEquiv ℂ (Fin 1)).toLinearMap.domRestrict + (MvPolynomial.degreeOfLE (Fin 1) ℂ (fun _ => n)))) + (fun q => + (MvPolynomial.mem_degreeOfLE_iff_degreeOf _).2 + (isMultiaffine_polarization n + (MvPolynomial.uniqueAlgEquiv ℂ (Fin 1) q.1))) + /-- The diagonal projection `Π↓ₙ`, obtained by identifying every polarization variable with the unique univariate variable. -/ noncomputable def diagonalProjection (n : ℕ) : @@ -220,6 +287,33 @@ theorem coe_diagonalProjectionDegreeBox_polarizationDegreeBox (MvPolynomial.uniqueAlgEquiv ℂ (Fin 1)).symm p rw [diagonalProjection_polarizationDegreeBox hp] +/-- Source-side equation (2.2): diagonal projection is a left inverse to the +linear polarization map on the one-variable degree box. -/ +theorem diagonalProjectionDegreeBox_comp_polarizationDegreeBoxLinearMap + {n : ℕ} + (q : MvPolynomial.degreeOfLE (Fin 1) ℂ (fun _ => n)) : + diagonalProjectionDegreeBox n (polarizationDegreeBoxLinearMap n q) = q := by + have hdeg : ∀ i, q.1.degreeOf i ≤ n := + (MvPolynomial.mem_degreeOfLE_iff_degreeOf q.1).mp q.2 + have hp : (MvPolynomial.uniqueAlgEquiv ℂ (Fin 1) q.1).natDegree ≤ n := by + calc + (MvPolynomial.uniqueAlgEquiv ℂ (Fin 1) q.1).natDegree = + q.1.degreeOf default := by + rw [← MvPolynomial.degreeOf_uniqueAlgEquiv_symm] + simp + _ ≤ n := hdeg default + have hdiag : + diagonalProjection n + (polarization n (MvPolynomial.uniqueAlgEquiv ℂ (Fin 1) q.1)) = + MvPolynomial.uniqueAlgEquiv ℂ (Fin 1) q.1 := + diagonalProjection_polarizationDegreeBox hp + apply Subtype.ext + change (MvPolynomial.uniqueAlgEquiv ℂ (Fin 1)).symm + (diagonalProjection n + (polarization n (MvPolynomial.uniqueAlgEquiv ℂ (Fin 1) q.1))) = q.1 + rw [hdiag] + exact (MvPolynomial.uniqueAlgEquiv ℂ (Fin 1)).symm_apply_apply q.1 + /-- Evaluation of a polarization in elementary symmetric functions. -/ theorem eval_polarization (n : ℕ) (p : ℂ[X]) (z : Fin n → ℂ) : MvPolynomial.eval z (polarization n p) = From d9eb16d5b8516c3ef30e149209d6db780cfd326a Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Mon, 3 Aug 2026 08:39:40 +0000 Subject: [PATCH 08/81] Define source-polarized degree-box operator --- RealRooted.lean | 1 + .../Applications/DegreeBoxPolarization.lean | 39 +++++++++++++++++++ 2 files changed, 40 insertions(+) create mode 100644 RealRooted/BorceaBranden/Applications/DegreeBoxPolarization.lean diff --git a/RealRooted.lean b/RealRooted.lean index 4bca6b204..86b3c2b47 100644 --- a/RealRooted.lean +++ b/RealRooted.lean @@ -34,6 +34,7 @@ import RealRooted.BorceaBranden.FiniteSymbolReconstruction import RealRooted.BorceaBranden.FiniteSymbolReconstructionCore import RealRooted.BorceaBranden.FiniteSymbolBasis import RealRooted.BorceaBranden.Applications.BidiagonalSymbol +import RealRooted.BorceaBranden.Applications.DegreeBoxPolarization import RealRooted.BorceaBranden.Applications.HomogenizeStable import RealRooted.BorceaBranden.Applications.UnivariateSymbol import RealRooted.CauchyInterlacing diff --git a/RealRooted/BorceaBranden/Applications/DegreeBoxPolarization.lean b/RealRooted/BorceaBranden/Applications/DegreeBoxPolarization.lean new file mode 100644 index 000000000..7d39ba9c8 --- /dev/null +++ b/RealRooted/BorceaBranden/Applications/DegreeBoxPolarization.lean @@ -0,0 +1,39 @@ +import RealRooted.Polarization + +/-! +# Source polarization for degree-box operators + +This file implements the source-side operator lift from Borcea--Brändén, +equation (2.2), for a one-variable degree-`n` source box. The lift first +diagonalizes a multiaffine input and then applies the original operator. +-/ + +namespace RealRooted.BorceaBranden + +noncomputable section + +/-- Lift an operator with a one-variable degree-`n` source to a multiaffine +`Fin n` source by precomposing with diagonal projection. -/ +def sourcePolarizedOperator {τ : Type*} (n : ℕ) + (T : MvPolynomial.degreeOfLE (Fin 1) ℂ (fun _ => n) →ₗ[ℂ] + MvPolynomial τ ℂ) : + MvPolynomial.degreeOfLE (Fin n) ℂ (fun _ => 1) →ₗ[ℂ] + MvPolynomial τ ℂ := + T.comp (diagonalProjectionDegreeBox n) + +/-- Source-side equation (2.2): restricting the lifted operator along source +polarization reconstructs the original operator. -/ +theorem sourcePolarizedOperator_comp_polarizationDegreeBoxLinearMap + {τ : Type*} {n : ℕ} + (T : MvPolynomial.degreeOfLE (Fin 1) ℂ (fun _ => n) →ₗ[ℂ] + MvPolynomial τ ℂ) : + (sourcePolarizedOperator n T).comp + (polarizationDegreeBoxLinearMap n) = T := by + ext q + change T (diagonalProjectionDegreeBox n + (polarizationDegreeBoxLinearMap n q)) = T q + rw [diagonalProjectionDegreeBox_comp_polarizationDegreeBoxLinearMap q] + +end + +end RealRooted.BorceaBranden From 6fdc02becaf294dda34ef35141fa1d02d43c8e35 Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Mon, 3 Aug 2026 08:40:52 +0000 Subject: [PATCH 09/81] Hide polarization linearity helpers --- RealRooted/Polarization.lean | 19 +++++++++---------- 1 file changed, 9 insertions(+), 10 deletions(-) diff --git a/RealRooted/Polarization.lean b/RealRooted/Polarization.lean index cad839438..0773c4132 100644 --- a/RealRooted/Polarization.lean +++ b/RealRooted/Polarization.lean @@ -59,23 +59,22 @@ elementary symmetric polynomial is `p.coeff k / choose n k`. -/ def polarization (n : ℕ) (p : ℂ[X]) : MvPolynomial (Fin n) ℂ := reducedPolarization n (binomialUnlift n p) -theorem binomialUnlift_add (n : ℕ) (p q : ℂ[X]) : +private theorem binomialUnlift_add (n : ℕ) (p q : ℂ[X]) : binomialUnlift n (p + q) = binomialUnlift n p + binomialUnlift n q := by unfold binomialUnlift rw [← Finset.sum_add_distrib] apply Finset.sum_congr rfl - intro k hk + intro k _ rw [Polynomial.coeff_add, add_div, map_add] -theorem binomialUnlift_smul (n : ℕ) (c : ℂ) (p : ℂ[X]) : +private theorem binomialUnlift_smul (n : ℕ) (c : ℂ) (p : ℂ[X]) : binomialUnlift n (c • p) = c • binomialUnlift n p := by unfold binomialUnlift rw [Finset.smul_sum] apply Finset.sum_congr rfl - intro k hk - simp only [Polynomial.coeff_smul] - simp only [div_eq_mul_inv] + intro k _ + simp only [Polynomial.coeff_smul, div_eq_mul_inv] change (Polynomial.monomial k) (c * p.coeff k * (n.choose k : ℂ)⁻¹) = c • (Polynomial.monomial k) @@ -84,21 +83,21 @@ theorem binomialUnlift_smul (n : ℕ) (c : ℂ) (p : ℂ[X]) : exact (Polynomial.smul_monomial c k (p.coeff k * (n.choose k : ℂ)⁻¹)).symm -theorem reducedPolarization_add (n : ℕ) (p q : ℂ[X]) : +private theorem reducedPolarization_add (n : ℕ) (p q : ℂ[X]) : reducedPolarization n (p + q) = reducedPolarization n p + reducedPolarization n q := by unfold reducedPolarization rw [← Finset.sum_add_distrib] apply Finset.sum_congr rfl - intro k hk + intro k _ simp [add_mul] -theorem reducedPolarization_smul (n : ℕ) (c : ℂ) (p : ℂ[X]) : +private theorem reducedPolarization_smul (n : ℕ) (c : ℂ) (p : ℂ[X]) : reducedPolarization n (c • p) = c • reducedPolarization n p := by unfold reducedPolarization rw [Finset.smul_sum] apply Finset.sum_congr rfl - intro k hk + intro k _ simp [MvPolynomial.smul_eq_C_mul, mul_assoc] /-- Polarization as a complex-linear map on univariate polynomials. -/ From 5c8391c4f26b1b7f7120d3698fa3f9c95ffe8f03 Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Mon, 3 Aug 2026 08:52:39 +0000 Subject: [PATCH 10/81] Specialize polarization degree equivalence --- RealRooted/Polarization.lean | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/RealRooted/Polarization.lean b/RealRooted/Polarization.lean index 0773c4132..1680b0f4f 100644 --- a/RealRooted/Polarization.lean +++ b/RealRooted/Polarization.lean @@ -298,8 +298,9 @@ theorem diagonalProjectionDegreeBox_comp_polarizationDegreeBoxLinearMap calc (MvPolynomial.uniqueAlgEquiv ℂ (Fin 1) q.1).natDegree = q.1.degreeOf default := by - rw [← MvPolynomial.degreeOf_uniqueAlgEquiv_symm] - simp + simpa only [AlgEquiv.symm_apply_apply] using + (MvPolynomial.degreeOf_uniqueAlgEquiv_symm (σ := Fin 1) + (MvPolynomial.uniqueAlgEquiv ℂ (Fin 1) q.1)).symm _ ≤ n := hdeg default have hdiag : diagonalProjection n From 33d0be625713d74f3ebd5ea23ddf003ad63eebe9 Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Mon, 3 Aug 2026 08:55:56 +0000 Subject: [PATCH 11/81] Normalize multiaffine symbol coefficients --- .../Algebra/MvPolynomial/Stability/Symbol.lean | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/RealRooted/Mathlib/Algebra/MvPolynomial/Stability/Symbol.lean b/RealRooted/Mathlib/Algebra/MvPolynomial/Stability/Symbol.lean index 131f6ce15..aa874e25a 100644 --- a/RealRooted/Mathlib/Algebra/MvPolynomial/Stability/Symbol.lean +++ b/RealRooted/Mathlib/Algebra/MvPolynomial/Stability/Symbol.lean @@ -40,6 +40,17 @@ variable {σ τ R : Type*} [CommSemiring R] [Fintype σ] def boxChoose (κ : σ → ℕ) (m : σ →₀ ℕ) : ℕ := ∏ i, Nat.choose (κ i) (m i) +/-- Every binomial coefficient in a multiaffine source box is one. -/ +@[simp] +theorem boxChoose_one_of_le_one (m : σ →₀ ℕ) (hm : ∀ i, m i ≤ 1) : + boxChoose (fun _ : σ => 1) m = 1 := by + classical + simp only [boxChoose] + apply Finset.prod_eq_one + intro i hi + have hle := hm i + interval_cases h : m i <;> simp + /-- The right-block monomial with exponent vector `κ - m`. -/ noncomputable def rightComplementMonomial (κ : σ → ℕ) (m : σ →₀ ℕ) : MvPolynomial (τ ⊕ σ) R := From aaee7e3093cacc564d3ebc386edb3df508fed1e3 Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Mon, 3 Aug 2026 09:01:15 +0000 Subject: [PATCH 12/81] Evaluate diagonal projection on basis monomials --- RealRooted/Polarization.lean | 34 ++++++++++++++++++++++++++++++++++ 1 file changed, 34 insertions(+) diff --git a/RealRooted/Polarization.lean b/RealRooted/Polarization.lean index 1680b0f4f..d9f52c1a6 100644 --- a/RealRooted/Polarization.lean +++ b/RealRooted/Polarization.lean @@ -429,4 +429,38 @@ theorem mvUpperHalfPlaneStable_polarization {n : ℕ} {p : ℂ[X]} end +private theorem uniqueAlgEquiv_rename_const_monomial + {R : Type*} [CommSemiring R] {n : ℕ} (m : Fin n →₀ ℕ) : + MvPolynomial.uniqueAlgEquiv R (Fin 1) + (MvPolynomial.rename (fun _ : Fin n => (0 : Fin 1)) + (MvPolynomial.monomial m 1)) = + Polynomial.X ^ m.degree := by + rw [MvPolynomial.rename_monomial, MvPolynomial.uniqueAlgEquiv_monomial] + rw [Polynomial.X_pow_eq_monomial] + apply congrArg (fun k : ℕ => Polynomial.monomial k (1 : R)) + calc + (Finsupp.mapDomain (fun _ : Fin n => (0 : Fin 1)) m) default = + m.sum (fun _ e => e) := by + simp [Finsupp.mapDomain, Finsupp.sum_apply] + _ = m.degree := by + rw [Finsupp.degree_apply] + rfl + +/-- Diagonal projection sends a bounded multiaffine basis monomial to the +univariate monomial whose exponent is its total degree. -/ +theorem diagonalProjection_basisDegreeOfLE {n : ℕ} + (m : {m : Fin n →₀ ℕ // ∀ i, m i ≤ 1}) : + diagonalProjection n + (MvPolynomial.basisDegreeOfLE (R := ℂ) (fun _ : Fin n => 1) m) = + Polynomial.X ^ m.1.degree := by + change MvPolynomial.uniqueAlgEquiv ℂ (Fin 1) + (MvPolynomial.rename (fun _ : Fin n => (0 : Fin 1)) + ((MvPolynomial.basisDegreeOfLE (R := ℂ) + (fun _ : Fin n => 1) m : + MvPolynomial.degreeOfLE (Fin n) ℂ (fun _ => 1)) : + MvPolynomial (Fin n) ℂ)) = + Polynomial.X ^ m.1.degree + rw [MvPolynomial.coe_basisDegreeOfLE] + exact uniqueAlgEquiv_rename_const_monomial m.1 + end RealRooted From b0161904b6564a6286ef5d6cdc7a2b17ef45e2f9 Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Mon, 3 Aug 2026 09:03:29 +0000 Subject: [PATCH 13/81] Inline diagonal monomial calculation --- RealRooted/Polarization.lean | 28 ++++++++++------------------ 1 file changed, 10 insertions(+), 18 deletions(-) diff --git a/RealRooted/Polarization.lean b/RealRooted/Polarization.lean index d9f52c1a6..63cf2b688 100644 --- a/RealRooted/Polarization.lean +++ b/RealRooted/Polarization.lean @@ -429,23 +429,6 @@ theorem mvUpperHalfPlaneStable_polarization {n : ℕ} {p : ℂ[X]} end -private theorem uniqueAlgEquiv_rename_const_monomial - {R : Type*} [CommSemiring R] {n : ℕ} (m : Fin n →₀ ℕ) : - MvPolynomial.uniqueAlgEquiv R (Fin 1) - (MvPolynomial.rename (fun _ : Fin n => (0 : Fin 1)) - (MvPolynomial.monomial m 1)) = - Polynomial.X ^ m.degree := by - rw [MvPolynomial.rename_monomial, MvPolynomial.uniqueAlgEquiv_monomial] - rw [Polynomial.X_pow_eq_monomial] - apply congrArg (fun k : ℕ => Polynomial.monomial k (1 : R)) - calc - (Finsupp.mapDomain (fun _ : Fin n => (0 : Fin 1)) m) default = - m.sum (fun _ e => e) := by - simp [Finsupp.mapDomain, Finsupp.sum_apply] - _ = m.degree := by - rw [Finsupp.degree_apply] - rfl - /-- Diagonal projection sends a bounded multiaffine basis monomial to the univariate monomial whose exponent is its total degree. -/ theorem diagonalProjection_basisDegreeOfLE {n : ℕ} @@ -461,6 +444,15 @@ theorem diagonalProjection_basisDegreeOfLE {n : ℕ} MvPolynomial (Fin n) ℂ)) = Polynomial.X ^ m.1.degree rw [MvPolynomial.coe_basisDegreeOfLE] - exact uniqueAlgEquiv_rename_const_monomial m.1 + rw [MvPolynomial.rename_monomial, MvPolynomial.uniqueAlgEquiv_monomial] + rw [Polynomial.X_pow_eq_monomial] + apply congrArg (fun k : ℕ => Polynomial.monomial k (1 : ℂ)) + calc + (Finsupp.mapDomain (fun _ : Fin n => (0 : Fin 1)) m.1) default = + m.1.sum (fun _ e => e) := by + simp [Finsupp.mapDomain, Finsupp.sum_apply] + _ = m.1.degree := by + rw [Finsupp.degree_apply] + rfl end RealRooted From 68cfa138f8acfdecf38ad0e2117d1b604624eb5b Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Mon, 3 Aug 2026 09:06:51 +0000 Subject: [PATCH 14/81] Lift polarized operators on basis monomials --- .../Applications/DegreeBoxPolarization.lean | 16 +++++++ RealRooted/Polarization.lean | 42 +++++++++++++++++++ 2 files changed, 58 insertions(+) diff --git a/RealRooted/BorceaBranden/Applications/DegreeBoxPolarization.lean b/RealRooted/BorceaBranden/Applications/DegreeBoxPolarization.lean index 7d39ba9c8..a4e787d93 100644 --- a/RealRooted/BorceaBranden/Applications/DegreeBoxPolarization.lean +++ b/RealRooted/BorceaBranden/Applications/DegreeBoxPolarization.lean @@ -34,6 +34,22 @@ theorem sourcePolarizedOperator_comp_polarizationDegreeBoxLinearMap (polarizationDegreeBoxLinearMap n q)) = T q rw [diagonalProjectionDegreeBox_comp_polarizationDegreeBoxLinearMap q] +/-- The source-polarized operator sends a multiaffine basis monomial to the +original operator applied to the one-variable basis monomial of the same total +degree. This is the basis-level content of Borcea--Branden Lemma 2.5. -/ +theorem sourcePolarizedOperator_basisDegreeOfLE + {τ : Type*} {n : ℕ} + (T : MvPolynomial.degreeOfLE (Fin 1) ℂ (fun _ => n) →ₗ[ℂ] + MvPolynomial τ ℂ) + (m : {m : Fin n →₀ ℕ // ∀ i, m i ≤ 1}) : + sourcePolarizedOperator n T + (MvPolynomial.basisDegreeOfLE (R := ℂ) (fun _ : Fin n => 1) m) = + T (MvPolynomial.basisDegreeOfLE (R := ℂ) (fun _ : Fin 1 => n) + (diagonalDegreeBoxIndex m)) := by + change T (diagonalProjectionDegreeBox n + (MvPolynomial.basisDegreeOfLE (R := ℂ) (fun _ : Fin n => 1) m)) = _ + rw [diagonalProjectionDegreeBox_basisDegreeOfLE] + end end RealRooted.BorceaBranden diff --git a/RealRooted/Polarization.lean b/RealRooted/Polarization.lean index 63cf2b688..be4d8a065 100644 --- a/RealRooted/Polarization.lean +++ b/RealRooted/Polarization.lean @@ -455,4 +455,46 @@ theorem diagonalProjection_basisDegreeOfLE {n : ℕ} rw [Finsupp.degree_apply] rfl +private theorem degree_le_fin_card_of_le_one {n : ℕ} + (m : Fin n →₀ ℕ) (hm : ∀ i, m i ≤ 1) : + m.degree ≤ n := by + rw [Finsupp.degree_apply] + calc + ∑ i ∈ m.support, m i ≤ ∑ i ∈ m.support, 1 := + Finset.sum_le_sum fun i hi => hm i + _ = m.support.card := by simp + _ ≤ Fintype.card (Fin n) := Finset.card_le_univ m.support + _ = n := Fintype.card_fin n + +/-- The one-variable degree-box index obtained by diagonalizing a bounded +multiaffine exponent vector. -/ +noncomputable def diagonalDegreeBoxIndex {n : ℕ} + (m : {m : Fin n →₀ ℕ // ∀ i, m i ≤ 1}) : + {d : Fin 1 →₀ ℕ // ∀ i, d i ≤ n} := + ⟨Finsupp.single default m.1.degree, fun i => by + rw [Subsingleton.elim i default, Finsupp.single_eq_same] + exact degree_le_fin_card_of_le_one m.1 m.2⟩ + +/-- Diagonal projection on degree boxes sends a multiaffine basis monomial to +the one-variable basis monomial indexed by its total degree. -/ +theorem diagonalProjectionDegreeBox_basisDegreeOfLE {n : ℕ} + (m : {m : Fin n →₀ ℕ // ∀ i, m i ≤ 1}) : + diagonalProjectionDegreeBox n + (MvPolynomial.basisDegreeOfLE (R := ℂ) (fun _ : Fin n => 1) m) = + MvPolynomial.basisDegreeOfLE (R := ℂ) (fun _ : Fin 1 => n) + (diagonalDegreeBoxIndex m) := by + apply Subtype.ext + change (MvPolynomial.uniqueAlgEquiv ℂ (Fin 1)).symm + (diagonalProjection n + (MvPolynomial.basisDegreeOfLE (R := ℂ) (fun _ : Fin n => 1) m)) = + ((MvPolynomial.basisDegreeOfLE (R := ℂ) (fun _ : Fin 1 => n) + (diagonalDegreeBoxIndex m) : + MvPolynomial.degreeOfLE (Fin 1) ℂ (fun _ => n)) : + MvPolynomial (Fin 1) ℂ) + apply (MvPolynomial.uniqueAlgEquiv ℂ (Fin 1)).injective + rw [AlgEquiv.apply_symm_apply, diagonalProjection_basisDegreeOfLE, + MvPolynomial.coe_basisDegreeOfLE, + MvPolynomial.uniqueAlgEquiv_monomial] + simp [diagonalDegreeBoxIndex, Polynomial.X_pow_eq_monomial] + end RealRooted From ba1377095b33d5b54713f4ea8fb42a39c6c746fb Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Mon, 3 Aug 2026 09:11:20 +0000 Subject: [PATCH 15/81] Reindex multiaffine exponents by support --- .../Applications/DegreeBoxPolarization.lean | 13 ++++++++ .../BorceaBranden/FiniteSymbolBasis.lean | 30 +++++++++++++++++++ 2 files changed, 43 insertions(+) diff --git a/RealRooted/BorceaBranden/Applications/DegreeBoxPolarization.lean b/RealRooted/BorceaBranden/Applications/DegreeBoxPolarization.lean index a4e787d93..9bc92f12f 100644 --- a/RealRooted/BorceaBranden/Applications/DegreeBoxPolarization.lean +++ b/RealRooted/BorceaBranden/Applications/DegreeBoxPolarization.lean @@ -1,3 +1,4 @@ +import RealRooted.BorceaBranden.FiniteSymbolBasis import RealRooted.Polarization /-! @@ -50,6 +51,18 @@ theorem sourcePolarizedOperator_basisDegreeOfLE (MvPolynomial.basisDegreeOfLE (R := ℂ) (fun _ : Fin n => 1) m)) = _ rw [diagonalProjectionDegreeBox_basisDegreeOfLE] +/-- Reindex a sum over multiaffine exponent vectors by their finite supports. +This is the subset reindexing in the source-side proof of Lemma 2.5. -/ +theorem sum_degreeOneExponent_eq_sum_finset + {M : Type*} [AddCommMonoid M] {n : ℕ} + (f : {m : Fin n →₀ ℕ // ∀ i, m i ≤ 1} → M) : + ∑ m, f m = + ∑ s : Finset (Fin n), + f ((degreeOneExponentEquivFinset (Fin n)).symm s) := by + apply Fintype.sum_equiv (degreeOneExponentEquivFinset (Fin n)) + intro m + simp + end end RealRooted.BorceaBranden diff --git a/RealRooted/BorceaBranden/FiniteSymbolBasis.lean b/RealRooted/BorceaBranden/FiniteSymbolBasis.lean index f26cb153f..9d841328b 100644 --- a/RealRooted/BorceaBranden/FiniteSymbolBasis.lean +++ b/RealRooted/BorceaBranden/FiniteSymbolBasis.lean @@ -48,6 +48,36 @@ theorem finsupp_eq_iff_support_eq_of_le_one rw [finsupp_eq_indicator_support_of_le_one d hd, finsupp_eq_indicator_support_of_le_one e he, hsupport] +/-- Natural-valued exponent vectors bounded by one are equivalent to finite +subsets, via their supports. -/ +noncomputable def degreeOneExponentEquivFinset (sigma : Type*) : + {d : sigma →₀ ℕ // ∀ i, d i ≤ 1} ≃ Finset sigma where + toFun d := d.1.support + invFun s := + ⟨Finsupp.indicator s (fun _ _ => 1), fun i => by + by_cases hi : i ∈ s <;> simp [Finsupp.indicator, hi]⟩ + left_inv d := + Subtype.ext (finsupp_eq_indicator_support_of_le_one d.1 d.2).symm + right_inv s := by + ext i + simp [Finsupp.indicator] + +/-- The total degree of a zero-one exponent vector is the cardinality of its +support. -/ +theorem card_support_eq_degree_of_le_one + {sigma : Type*} (d : sigma →₀ ℕ) (hd : ∀ i, d i ≤ 1) : + d.support.card = d.degree := by + classical + rw [Finsupp.degree_apply] + calc + d.support.card = ∑ i ∈ d.support, 1 := by simp + _ = ∑ i ∈ d.support, d i := by + apply Finset.sum_congr rfl + intro i hi + have hpos : 0 < d i := Finsupp.mem_support_iff.mp hi |>.bot_lt + have hone : d i = 1 := Nat.le_antisymm (hd i) hpos + simp [hone] + end end RealRooted.BorceaBranden From 0b5c6b7fc6a35107fcc8b99aedd53106642bb26e Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Mon, 3 Aug 2026 09:13:16 +0000 Subject: [PATCH 16/81] Golf zero-one exponent normalization --- RealRooted/BorceaBranden/FiniteSymbolBasis.lean | 16 ++-------------- 1 file changed, 2 insertions(+), 14 deletions(-) diff --git a/RealRooted/BorceaBranden/FiniteSymbolBasis.lean b/RealRooted/BorceaBranden/FiniteSymbolBasis.lean index 9d841328b..8ec46a101 100644 --- a/RealRooted/BorceaBranden/FiniteSymbolBasis.lean +++ b/RealRooted/BorceaBranden/FiniteSymbolBasis.lean @@ -20,20 +20,8 @@ theorem finsupp_eq_indicator_support_of_le_one d = Finsupp.indicator d.support (fun _ _ => 1) := by classical ext i - by_cases hi : i ∈ d.support - · rw [Finsupp.indicator_of_mem hi] - have hne : d i ≠ 0 := Finsupp.mem_support_iff.mp hi - have hle := hd i - cases hdi : d i with - | zero => exact (hne hdi).elim - | succ n => - cases n with - | zero => rfl - | succ n => - rw [hdi] at hle - exact (Nat.not_succ_le_zero n (Nat.le_of_succ_le_succ hle)).elim - · rw [Finsupp.indicator_of_notMem hi] - simpa [Finsupp.mem_support_iff] using hi + have hle := hd i + interval_cases h : d i <;> simp [Finsupp.indicator, h] /-- Coordinate-wise degree-one exponent vectors are equal exactly when their supports are equal. -/ From 8589704d388b8b020deccb2e970424cd2edd6e7b Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Mon, 3 Aug 2026 09:16:44 +0000 Subject: [PATCH 17/81] Group multiaffine terms by total degree --- .../Applications/DegreeBoxPolarization.lean | 32 +++++++++++++++++ .../BorceaBranden/FiniteSymbolBasis.lean | 34 +++++++++++++------ 2 files changed, 56 insertions(+), 10 deletions(-) diff --git a/RealRooted/BorceaBranden/Applications/DegreeBoxPolarization.lean b/RealRooted/BorceaBranden/Applications/DegreeBoxPolarization.lean index 9bc92f12f..ce3db7ab2 100644 --- a/RealRooted/BorceaBranden/Applications/DegreeBoxPolarization.lean +++ b/RealRooted/BorceaBranden/Applications/DegreeBoxPolarization.lean @@ -63,6 +63,38 @@ theorem sum_degreeOneExponent_eq_sum_finset intro m simp +/-- Partition a sum over subsets of `Fin n` by subset cardinality. -/ +theorem sum_finset_eq_sum_powersetCard + {M : Type*} [AddCommMonoid M] (n : ℕ) + (f : Finset (Fin n) → M) : + ∑ s, f s = + ∑ k ∈ Finset.range (n + 1), + ∑ s ∈ (Finset.univ : Finset (Fin n)).powersetCard k, f s := by + simpa using + Finset.sum_powerset (Finset.univ : Finset (Fin n)) f + +/-- Summing a cardinality-dependent contribution over subsets of `Fin n` +produces the corresponding binomial coefficients. -/ +theorem sum_finset_cardFunction + {M : Type*} [AddCommMonoid M] (n : ℕ) (g : ℕ → M) : + ∑ s : Finset (Fin n), g s.card = + ∑ k ∈ Finset.range (n + 1), n.choose k • g k := by + rw [sum_finset_eq_sum_powersetCard] + apply Finset.sum_congr rfl + intro k hk + simpa using + Finset.sum_powersetCard k (Finset.univ : Finset (Fin n)) g + +/-- The coefficient grouping for multiaffine source exponents: one term for +each zero-one exponent vector becomes `choose n k` copies of the contribution +of total degree `k`. -/ +theorem sum_degreeOneExponent_degreeFunction + {M : Type*} [AddCommMonoid M] (n : ℕ) (g : ℕ → M) : + ∑ m : {m : Fin n →₀ ℕ // ∀ i, m i ≤ 1}, g m.1.degree = + ∑ k ∈ Finset.range (n + 1), n.choose k • g k := by + rw [sum_degreeOneExponent_eq_sum_finset] + simpa using sum_finset_cardFunction n g + end end RealRooted.BorceaBranden diff --git a/RealRooted/BorceaBranden/FiniteSymbolBasis.lean b/RealRooted/BorceaBranden/FiniteSymbolBasis.lean index 8ec46a101..de4269f9a 100644 --- a/RealRooted/BorceaBranden/FiniteSymbolBasis.lean +++ b/RealRooted/BorceaBranden/FiniteSymbolBasis.lean @@ -39,16 +39,18 @@ theorem finsupp_eq_iff_support_eq_of_le_one /-- Natural-valued exponent vectors bounded by one are equivalent to finite subsets, via their supports. -/ noncomputable def degreeOneExponentEquivFinset (sigma : Type*) : - {d : sigma →₀ ℕ // ∀ i, d i ≤ 1} ≃ Finset sigma where - toFun d := d.1.support - invFun s := - ⟨Finsupp.indicator s (fun _ _ => 1), fun i => by - by_cases hi : i ∈ s <;> simp [Finsupp.indicator, hi]⟩ - left_inv d := - Subtype.ext (finsupp_eq_indicator_support_of_le_one d.1 d.2).symm - right_inv s := by - ext i - simp [Finsupp.indicator] + {d : sigma →₀ ℕ // ∀ i, d i ≤ 1} ≃ Finset sigma := by + classical + exact + { toFun := fun d => d.1.support + invFun := fun s => + ⟨Finsupp.indicator s (fun _ _ => 1), fun i => by + by_cases hi : i ∈ s <;> simp [Finsupp.indicator, hi]⟩ + left_inv := fun d => + Subtype.ext (finsupp_eq_indicator_support_of_le_one d.1 d.2).symm + right_inv := fun s => by + ext i + simp [Finsupp.indicator] } /-- The total degree of a zero-one exponent vector is the cardinality of its support. -/ @@ -66,6 +68,18 @@ theorem card_support_eq_degree_of_le_one have hone : d i = 1 := Nat.le_antisymm (hd i) hpos simp [hone] +@[simp] +theorem degree_degreeOneExponentEquivFinset_symm + {sigma : Type*} (s : Finset sigma) : + ((degreeOneExponentEquivFinset sigma).symm s).1.degree = s.card := by + let d := (degreeOneExponentEquivFinset sigma).symm s + have hsupp : d.1.support = s := + (degreeOneExponentEquivFinset sigma).apply_symm_apply s + calc + d.1.degree = d.1.support.card := + (card_support_eq_degree_of_le_one d.1 d.2).symm + _ = s.card := congrArg Finset.card hsupp + end end RealRooted.BorceaBranden From ca03f25cbd60fd43d0bb2f4bc4a86b4588c2f619 Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Mon, 3 Aug 2026 09:22:04 +0000 Subject: [PATCH 18/81] Diagonalize complementary symbol monomials --- .../Applications/DegreeBoxPolarization.lean | 26 +++++++++++++++++++ .../BorceaBranden/FiniteSymbolBasis.lean | 19 ++++++++++++++ 2 files changed, 45 insertions(+) diff --git a/RealRooted/BorceaBranden/Applications/DegreeBoxPolarization.lean b/RealRooted/BorceaBranden/Applications/DegreeBoxPolarization.lean index ce3db7ab2..ea4e7f5bc 100644 --- a/RealRooted/BorceaBranden/Applications/DegreeBoxPolarization.lean +++ b/RealRooted/BorceaBranden/Applications/DegreeBoxPolarization.lean @@ -98,3 +98,29 @@ theorem sum_degreeOneExponent_degreeFunction end end RealRooted.BorceaBranden + +namespace MvPolynomial + +/-- Identify all polarized source variables while leaving output variables +unchanged. -/ +def sourceDiagonalVariableMap {τ : Type*} {n : ℕ} : + τ ⊕ Fin n → τ ⊕ Fin 1 + | Sum.inl i => Sum.inl i + | Sum.inr _ => Sum.inr default + +/-- Diagonalizing a complementary zero-one source monomial records only its +complementary total degree. -/ +theorem rename_rightComplementMonomial_one + {τ : Type*} {n : ℕ} (m : Fin n →₀ ℕ) + (hm : ∀ i, m i ≤ 1) : + rename (sourceDiagonalVariableMap (τ := τ) (n := n)) + (rightComplementMonomial (R := ℂ) (τ := τ) + (fun _ : Fin n => 1) m) = + X (Sum.inr default) ^ (n - m.degree) := by + rw [rightComplementMonomial_eq_prod] + simp only [map_prod, map_pow, rename_X, sourceDiagonalVariableMap] + rw [Finset.prod_pow_eq_pow_sum] + congr 1 + simpa using sum_one_sub_eq_card_sub_degree m hm + +end MvPolynomial diff --git a/RealRooted/BorceaBranden/FiniteSymbolBasis.lean b/RealRooted/BorceaBranden/FiniteSymbolBasis.lean index de4269f9a..90bd9437e 100644 --- a/RealRooted/BorceaBranden/FiniteSymbolBasis.lean +++ b/RealRooted/BorceaBranden/FiniteSymbolBasis.lean @@ -83,3 +83,22 @@ theorem degree_degreeOneExponentEquivFinset_symm end end RealRooted.BorceaBranden + +namespace MvPolynomial + +/-- The complement of a zero-one exponent has total degree equal to the +cardinality of the variable set minus the original total degree. -/ +theorem sum_one_sub_eq_card_sub_degree + {σ : Type*} [Fintype σ] (m : σ →₀ ℕ) + (hm : ∀ i, m i ≤ 1) : + ∑ i, (1 - m i) = Fintype.card σ - m.degree := by + rw [Finset.sum_tsub_distrib Finset.univ (by + intro i hi + exact hm i)] + simp only [Finset.sum_const, Finset.card_univ, nsmul_eq_mul, + Nat.mul_one] + congr 1 + rw [Finsupp.degree_apply] + exact (Finsupp.sum_fintype m (fun _ e => e) (fun _ => rfl)).symm + +end MvPolynomial From e1e0ac4f5f6625ac31ba7dc4fcc1234b49d80094 Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Mon, 3 Aug 2026 09:23:32 +0000 Subject: [PATCH 19/81] Place complement degree lemma in Finsupp --- .../Applications/DegreeBoxPolarization.lean | 2 +- RealRooted/BorceaBranden/FiniteSymbolBasis.lean | 10 +++++----- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/RealRooted/BorceaBranden/Applications/DegreeBoxPolarization.lean b/RealRooted/BorceaBranden/Applications/DegreeBoxPolarization.lean index ea4e7f5bc..fe42d371c 100644 --- a/RealRooted/BorceaBranden/Applications/DegreeBoxPolarization.lean +++ b/RealRooted/BorceaBranden/Applications/DegreeBoxPolarization.lean @@ -121,6 +121,6 @@ theorem rename_rightComplementMonomial_one simp only [map_prod, map_pow, rename_X, sourceDiagonalVariableMap] rw [Finset.prod_pow_eq_pow_sum] congr 1 - simpa using sum_one_sub_eq_card_sub_degree m hm + simpa using Finsupp.sum_one_sub_eq_card_sub_degree m hm end MvPolynomial diff --git a/RealRooted/BorceaBranden/FiniteSymbolBasis.lean b/RealRooted/BorceaBranden/FiniteSymbolBasis.lean index 90bd9437e..484b7bc39 100644 --- a/RealRooted/BorceaBranden/FiniteSymbolBasis.lean +++ b/RealRooted/BorceaBranden/FiniteSymbolBasis.lean @@ -84,7 +84,7 @@ end end RealRooted.BorceaBranden -namespace MvPolynomial +namespace Finsupp /-- The complement of a zero-one exponent has total degree equal to the cardinality of the variable set minus the original total degree. -/ @@ -93,12 +93,12 @@ theorem sum_one_sub_eq_card_sub_degree (hm : ∀ i, m i ≤ 1) : ∑ i, (1 - m i) = Fintype.card σ - m.degree := by rw [Finset.sum_tsub_distrib Finset.univ (by - intro i hi + intro i _ exact hm i)] simp only [Finset.sum_const, Finset.card_univ, nsmul_eq_mul, Nat.mul_one] congr 1 - rw [Finsupp.degree_apply] - exact (Finsupp.sum_fintype m (fun _ e => e) (fun _ => rfl)).symm + rw [degree_apply] + exact (sum_fintype m (fun _ e => e) (fun _ => rfl)).symm -end MvPolynomial +end Finsupp From 3086ae9233b6d79dfe2db1bd65a4990cbf76c9f8 Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Mon, 3 Aug 2026 09:33:09 +0000 Subject: [PATCH 20/81] Prepare source symbol reindexing --- .../Applications/DegreeBoxPolarization.lean | 10 +++++++ .../Applications/UnivariateSymbol.lean | 10 +------ .../BorceaBranden/FiniteSymbolBasis.lean | 30 +++++++++++++++++++ 3 files changed, 41 insertions(+), 9 deletions(-) diff --git a/RealRooted/BorceaBranden/Applications/DegreeBoxPolarization.lean b/RealRooted/BorceaBranden/Applications/DegreeBoxPolarization.lean index fe42d371c..b3b272a27 100644 --- a/RealRooted/BorceaBranden/Applications/DegreeBoxPolarization.lean +++ b/RealRooted/BorceaBranden/Applications/DegreeBoxPolarization.lean @@ -108,6 +108,16 @@ def sourceDiagonalVariableMap {τ : Type*} {n : ℕ} : | Sum.inl i => Sum.inl i | Sum.inr _ => Sum.inr default +/-- Diagonalizing source variables leaves the output-variable block +unchanged. -/ +@[simp] theorem rename_sourceDiagonalVariableMap_rename_inl + {τ : Type*} {n : ℕ} (p : MvPolynomial τ ℂ) : + rename (sourceDiagonalVariableMap (τ := τ) (n := n)) + (rename (Sum.inl : τ → τ ⊕ Fin n) p) = + rename (Sum.inl : τ → τ ⊕ Fin 1) p := by + rw [rename_rename] + rfl + /-- Diagonalizing a complementary zero-one source monomial records only its complementary total degree. -/ theorem rename_rightComplementMonomial_one diff --git a/RealRooted/BorceaBranden/Applications/UnivariateSymbol.lean b/RealRooted/BorceaBranden/Applications/UnivariateSymbol.lean index d20a5a9a4..46f69b77e 100644 --- a/RealRooted/BorceaBranden/Applications/UnivariateSymbol.lean +++ b/RealRooted/BorceaBranden/Applications/UnivariateSymbol.lean @@ -1,5 +1,6 @@ import RealRooted.Mathlib.Algebra.MvPolynomial.Stability.Symbol import RealRooted.Challenges.BorceaBranden +import RealRooted.BorceaBranden.FiniteSymbolBasis /-! # Univariate compatibility for finite algebraic symbols @@ -33,11 +34,6 @@ noncomputable def univariateDegreeBoxOperator (d : ℕ) (T : ℝ[X] →ₗ[ℝ] map_add' p q := by simp map_smul' r p := by simp -/-- Bounded exponent vectors in one variable are indexed by `Fin (d + 1)`. -/ -noncomputable def degreeOfLEFinOneEquiv (d : ℕ) : - {m : Fin 1 →₀ ℕ // ∀ i, m i ≤ d} ≃ Fin (d + 1) := - (degreeOfLEIndexEquiv (fun _ : Fin 1 => d)).trans (Equiv.piUnique _) - lemma rename_uniqueAlgEquiv_symm_eq_polynomialInFirstMv (p : ℝ[X]) : rename finOneSumToFinTwo (rename (Sum.inl : Fin 1 → Fin 1 ⊕ Fin 1) @@ -61,10 +57,6 @@ lemma rename_rightComplementMonomial_finOne (d : ℕ) (m : Fin 1 →₀ ℕ) : X (1 : Fin 2) ^ (d - m 0) := by simp [rightComplementMonomial, finOneSumToFinTwo] -lemma degreeOfLEFinOneEquiv_val (d : ℕ) (m : {m : Fin 1 →₀ ℕ // ∀ i, m i ≤ d}) : - (degreeOfLEFinOneEquiv d m : ℕ) = m.1 0 := by - rfl - lemma univariateDegreeBoxOperator_basis (d : ℕ) (T : ℝ[X] →ₗ[ℝ] ℝ[X]) (m : {m : Fin 1 →₀ ℕ // ∀ i, m i ≤ d}) : univariateDegreeBoxOperator d T diff --git a/RealRooted/BorceaBranden/FiniteSymbolBasis.lean b/RealRooted/BorceaBranden/FiniteSymbolBasis.lean index 484b7bc39..198e91445 100644 --- a/RealRooted/BorceaBranden/FiniteSymbolBasis.lean +++ b/RealRooted/BorceaBranden/FiniteSymbolBasis.lean @@ -1,4 +1,5 @@ import RealRooted.BorceaBranden.FiniteSymbolCoefficient +import RealRooted.Mathlib.Algebra.MvPolynomial.Stability.DegreeBox /-! # Degree-one exponent coordinates for finite symbols @@ -86,6 +87,20 @@ end RealRooted.BorceaBranden namespace Finsupp +/-- A one-variable exponent vector is the singleton at its total degree. -/ +@[simp] theorem single_default_degree_fin_one (m : Fin 1 →₀ ℕ) : + single default m.degree = m := by + have hdegree : m.degree = ∑ i, m i := by + rw [degree_apply] + apply Finset.sum_subset (Finset.subset_univ m.support) + intro i _ hi + simpa [mem_support_iff] using hi + apply Finsupp.ext + intro i + fin_cases i + rw [hdegree] + simp + /-- The complement of a zero-one exponent has total degree equal to the cardinality of the variable set minus the original total degree. -/ theorem sum_one_sub_eq_card_sub_degree @@ -102,3 +117,18 @@ theorem sum_one_sub_eq_card_sub_degree exact (sum_fintype m (fun _ e => e) (fun _ => rfl)).symm end Finsupp + +namespace RealRooted.BorceaBranden + +/-- Bounded exponent vectors in one variable are indexed by `Fin (d + 1)`. -/ +noncomputable def degreeOfLEFinOneEquiv (d : ℕ) : + {m : Fin 1 →₀ ℕ // ∀ i, m i ≤ d} ≃ Fin (d + 1) := + (MvPolynomial.degreeOfLEIndexEquiv (fun _ : Fin 1 => d)).trans + (Equiv.piUnique _) + +lemma degreeOfLEFinOneEquiv_val (d : ℕ) + (m : {m : Fin 1 →₀ ℕ // ∀ i, m i ≤ d}) : + (degreeOfLEFinOneEquiv d m : ℕ) = m.1 0 := by + rfl + +end RealRooted.BorceaBranden From 4f93fa72b5ba1999a36a1f4b73a6ce149cfcebc6 Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Mon, 3 Aug 2026 09:47:09 +0000 Subject: [PATCH 21/81] Prove source polarized symbol identity --- .../Applications/DegreeBoxPolarization.lean | 81 +++++++++++++++++++ .../BorceaBranden/FiniteSymbolBasis.lean | 65 +++++++++++++++ 2 files changed, 146 insertions(+) diff --git a/RealRooted/BorceaBranden/Applications/DegreeBoxPolarization.lean b/RealRooted/BorceaBranden/Applications/DegreeBoxPolarization.lean index b3b272a27..c2915db1b 100644 --- a/RealRooted/BorceaBranden/Applications/DegreeBoxPolarization.lean +++ b/RealRooted/BorceaBranden/Applications/DegreeBoxPolarization.lean @@ -134,3 +134,84 @@ theorem rename_rightComplementMonomial_one simpa using Finsupp.sum_one_sub_eq_card_sub_degree m hm end MvPolynomial + +namespace RealRooted.BorceaBranden + +noncomputable section + +open MvPolynomial + +lemma finOneDegreeIndex_degree_eq_diagonalDegreeBoxIndex + {n : ℕ} (m : {m : Fin n →₀ ℕ // ∀ i, m i ≤ 1}) : + finOneDegreeIndex n m.1.degree = diagonalDegreeBoxIndex m := by + apply (degreeOfLEFinOneEquiv n).injective + apply Fin.ext + simp [finOneDegreeIndex, degreeOfLEFinOneEquiv_val, + diagonalDegreeBoxIndex, + Nat.min_eq_left (degree_le_fin_card_of_le_one m.1 m.2)] + +/-- Termwise form of the source-polarized algebraic symbol after identifying +all polarized source variables. -/ +theorem rename_algebraicSymbol_sourcePolarizedOperator_eq_sum + {τ : Type*} (n : ℕ) + (T : degreeOfLE (Fin 1) ℂ (fun _ => n) →ₗ[ℂ] + MvPolynomial τ ℂ) : + MvPolynomial.rename + (MvPolynomial.sourceDiagonalVariableMap (τ := τ) (n := n)) + (algebraicSymbol (fun _ : Fin n => 1) + (sourcePolarizedOperator n T)) = + ∑ m : {m : Fin n →₀ ℕ // ∀ i, m i ≤ 1}, + rename (Sum.inl : τ → τ ⊕ Fin 1) + (T (basisDegreeOfLE (R := ℂ) (fun _ : Fin 1 => n) + (diagonalDegreeBoxIndex m))) * + X (Sum.inr default) ^ (n - m.1.degree) := by + classical + rw [algebraicSymbol, map_sum] + apply Finset.sum_congr rfl + intro m _ + simp only [map_mul, rename_C] + rw [boxChoose_one_of_le_one m.1 m.2, Nat.cast_one, map_one, + one_mul, MvPolynomial.rename_sourceDiagonalVariableMap_rename_inl, + sourcePolarizedOperator_basisDegreeOfLE, + MvPolynomial.rename_rightComplementMonomial_one m.1 m.2] + +/-- Source-side specialization of Borcea--Brändén Lemma 2.5: diagonalizing the +multiaffine source symbol recovers the original degree-box symbol. -/ +theorem rename_algebraicSymbol_sourcePolarizedOperator + {τ : Type*} (n : ℕ) + (T : degreeOfLE (Fin 1) ℂ (fun _ => n) →ₗ[ℂ] + MvPolynomial τ ℂ) : + MvPolynomial.rename + (MvPolynomial.sourceDiagonalVariableMap (τ := τ) (n := n)) + (algebraicSymbol (fun _ : Fin n => 1) + (sourcePolarizedOperator n T)) = + algebraicSymbol (fun _ : Fin 1 => n) T := by + classical + let g : ℕ → MvPolynomial (τ ⊕ Fin 1) ℂ := fun k => + rename (Sum.inl : τ → τ ⊕ Fin 1) + (T (basisDegreeOfLE (R := ℂ) (fun _ : Fin 1 => n) + (finOneDegreeIndex n k))) * + X (Sum.inr default) ^ (n - k) + calc + MvPolynomial.rename + (MvPolynomial.sourceDiagonalVariableMap (τ := τ) (n := n)) + (algebraicSymbol (fun _ : Fin n => 1) + (sourcePolarizedOperator n T)) = + ∑ m : {m : Fin n →₀ ℕ // ∀ i, m i ≤ 1}, + g m.1.degree := by + rw [rename_algebraicSymbol_sourcePolarizedOperator_eq_sum] + apply Finset.sum_congr rfl + intro m _ + simp only [g] + rw [finOneDegreeIndex_degree_eq_diagonalDegreeBoxIndex] + _ = ∑ k ∈ Finset.range (n + 1), n.choose k • g k := + sum_degreeOneExponent_degreeFunction n g + _ = algebraicSymbol (fun _ : Fin 1 => n) T := by + rw [algebraicSymbol_finOne_eq_sum_range] + apply Finset.sum_congr rfl + intro k _ + simp [g, mul_assoc] + +end + +end RealRooted.BorceaBranden diff --git a/RealRooted/BorceaBranden/FiniteSymbolBasis.lean b/RealRooted/BorceaBranden/FiniteSymbolBasis.lean index 198e91445..66815b4d8 100644 --- a/RealRooted/BorceaBranden/FiniteSymbolBasis.lean +++ b/RealRooted/BorceaBranden/FiniteSymbolBasis.lean @@ -132,3 +132,68 @@ lemma degreeOfLEFinOneEquiv_val (d : ℕ) rfl end RealRooted.BorceaBranden + +namespace RealRooted.BorceaBranden + +noncomputable section + +open MvPolynomial + +/-- The canonical one-variable degree-box index associated with a natural +number. The truncation is inactive on `Fin (n + 1)`. -/ +noncomputable def finOneDegreeIndex (n k : ℕ) : + {m : Fin 1 →₀ ℕ // ∀ i, m i ≤ n} := + (degreeOfLEFinOneEquiv n).symm + ⟨min k n, Nat.lt_succ_iff.mpr (Nat.min_le_right k n)⟩ + +@[simp] lemma finOneDegreeIndex_equiv_apply (n : ℕ) + (m : {m : Fin 1 →₀ ℕ // ∀ i, m i ≤ n}) : + finOneDegreeIndex n (degreeOfLEFinOneEquiv n m) = m := by + apply (degreeOfLEFinOneEquiv n).injective + apply Fin.ext + simp [finOneDegreeIndex, degreeOfLEFinOneEquiv_val, m.2 0] + +/-- Expand a one-variable algebraic symbol over its canonical `Fin (n + 1)` +indexing. -/ +theorem algebraicSymbol_finOne_eq_sum_fin + {τ R : Type*} [CommSemiring R] (n : ℕ) + (T : degreeOfLE (Fin 1) R (fun _ => n) →ₗ[R] MvPolynomial τ R) : + algebraicSymbol (fun _ : Fin 1 => n) T = + ∑ k : Fin (n + 1), + C (n.choose k : R) * + rename (Sum.inl : τ → τ ⊕ Fin 1) + (T (basisDegreeOfLE (R := R) (fun _ : Fin 1 => n) + (finOneDegreeIndex n k))) * + X (Sum.inr default) ^ (n - k) := by + classical + rw [algebraicSymbol] + apply Fintype.sum_equiv (degreeOfLEFinOneEquiv n) + intro m + simp [finOneDegreeIndex_equiv_apply, boxChoose, + rightComplementMonomial, degreeOfLEFinOneEquiv_val] + +/-- Expand a one-variable algebraic symbol over the natural-number range +`0, ..., n`. -/ +theorem algebraicSymbol_finOne_eq_sum_range + {τ R : Type*} [CommSemiring R] (n : ℕ) + (T : degreeOfLE (Fin 1) R (fun _ => n) →ₗ[R] MvPolynomial τ R) : + algebraicSymbol (fun _ : Fin 1 => n) T = + ∑ k ∈ Finset.range (n + 1), + C (n.choose k : R) * + rename (Sum.inl : τ → τ ⊕ Fin 1) + (T (basisDegreeOfLE (R := R) (fun _ : Fin 1 => n) + (finOneDegreeIndex n k))) * + X (Sum.inr default) ^ (n - k) := by + classical + let g : ℕ → MvPolynomial (τ ⊕ Fin 1) R := fun k => + C (n.choose k : R) * + rename (Sum.inl : τ → τ ⊕ Fin 1) + (T (basisDegreeOfLE (R := R) (fun _ : Fin 1 => n) + (finOneDegreeIndex n k))) * + X (Sum.inr default) ^ (n - k) + rw [algebraicSymbol_finOne_eq_sum_fin (n := n) (T := T)] + simpa [g] using Fin.sum_univ_eq_sum_range g (n + 1) + +end + +end RealRooted.BorceaBranden From 554e81a840328a5eb81debf9d46d760dd261a9e0 Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Mon, 3 Aug 2026 10:03:29 +0000 Subject: [PATCH 22/81] Prove symmetry of polarization --- RealRooted/Polarization.lean | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) diff --git a/RealRooted/Polarization.lean b/RealRooted/Polarization.lean index be4d8a065..59d412ad4 100644 --- a/RealRooted/Polarization.lean +++ b/RealRooted/Polarization.lean @@ -498,3 +498,21 @@ theorem diagonalProjectionDegreeBox_basisDegreeOfLE {n : ℕ} simp [diagonalDegreeBoxIndex, Polynomial.X_pow_eq_monomial] end RealRooted + +namespace RealRooted + +/-- Reduced polarization is symmetric in its polarized variables. -/ +theorem isSymmetric_reducedPolarization (n : ℕ) (f : ℂ[X]) : + MvPolynomial.IsSymmetric (reducedPolarization n f) := by + classical + intro e + simp only [reducedPolarization, map_sum, map_mul, + MvPolynomial.rename_C, MvPolynomial.rename_esymm] + +/-- Polarization is symmetric in its polarized variables. -/ +theorem isSymmetric_polarization (n : ℕ) (p : ℂ[X]) : + MvPolynomial.IsSymmetric (polarization n p) := by + unfold polarization + exact isSymmetric_reducedPolarization n (binomialUnlift n p) + +end RealRooted From c4b26094bbf36a2439456673bd0966fd5a42db25 Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Mon, 3 Aug 2026 10:18:55 +0000 Subject: [PATCH 23/81] Add full polynomial symmetrization --- .../RingTheory/MvPolynomial/Symmetric.lean | 67 +++++++++++++++++++ RealRooted/Polarization.lean | 1 + 2 files changed, 68 insertions(+) create mode 100644 RealRooted/Mathlib/RingTheory/MvPolynomial/Symmetric.lean diff --git a/RealRooted/Mathlib/RingTheory/MvPolynomial/Symmetric.lean b/RealRooted/Mathlib/RingTheory/MvPolynomial/Symmetric.lean new file mode 100644 index 000000000..35b7f5ca4 --- /dev/null +++ b/RealRooted/Mathlib/RingTheory/MvPolynomial/Symmetric.lean @@ -0,0 +1,67 @@ +import Mathlib.RingTheory.MvPolynomial.Symmetric.Defs + +/-! +# Finite-variable symmetrization + +This file defines permutation summation and normalized symmetrization for +multivariate polynomials. These are the algebraic operators used in the +Grace--Walsh--Szegő symmetrization argument. +-/ + +open BigOperators + +namespace MvPolynomial + +/-- Sum all variable permutations of a multivariate polynomial. -/ +noncomputable def symmetrizationSum + {σ R : Type*} [Fintype σ] [CommSemiring R] + (p : MvPolynomial σ R) : MvPolynomial σ R := by + classical + exact ∑ e : Equiv.Perm σ, rename e p + +/-- The permutation sum is symmetric. -/ +theorem isSymmetric_symmetrizationSum + {σ R : Type*} [Fintype σ] [CommSemiring R] + (p : MvPolynomial σ R) : + IsSymmetric (symmetrizationSum p) := by + classical + intro e + simp only [symmetrizationSum, map_sum, rename_rename] + simpa [Function.comp_def] using + Equiv.sum_comp (Equiv.mulLeft e) + (fun f : Equiv.Perm σ => rename f p) + +/-- Average all variable permutations of a complex multivariate polynomial. -/ +noncomputable def fullSymmetrization + {σ : Type*} [Fintype σ] (p : MvPolynomial σ ℂ) : + MvPolynomial σ ℂ := by + classical + exact C (Fintype.card (Equiv.Perm σ) : ℂ)⁻¹ * + symmetrizationSum p + +/-- Full symmetrization is symmetric. -/ +theorem isSymmetric_fullSymmetrization + {σ : Type*} [Fintype σ] (p : MvPolynomial σ ℂ) : + IsSymmetric (fullSymmetrization p) := by + classical + intro e + simp only [fullSymmetrization, map_mul, rename_C] + rw [isSymmetric_symmetrizationSum p e] + +/-- Full symmetrization preserves evaluation at a constant assignment. -/ +theorem eval_const_fullSymmetrization + {σ : Type*} [Fintype σ] (p : MvPolynomial σ ℂ) (w : ℂ) : + eval (fun _ : σ => w) (fullSymmetrization p) = + eval (fun _ : σ => w) p := by + classical + have hcard : (Fintype.card (Equiv.Perm σ) : ℂ) ≠ 0 := by + exact_mod_cast Fintype.card_ne_zero + have hconst (e : Equiv.Perm σ) : + (fun _ : σ => w) ∘ e = fun _ : σ => w := by + rfl + simp only [fullSymmetrization, map_mul, eval_C, + symmetrizationSum, map_sum, eval_rename, hconst] + rw [Finset.sum_const, Finset.card_univ, nsmul_eq_mul, + ← mul_assoc, inv_mul_cancel₀ hcard, one_mul] + +end MvPolynomial diff --git a/RealRooted/Polarization.lean b/RealRooted/Polarization.lean index 59d412ad4..da35ab062 100644 --- a/RealRooted/Polarization.lean +++ b/RealRooted/Polarization.lean @@ -4,6 +4,7 @@ import RealRooted.Mathlib.Algebra.MvPolynomial.Stability.DegreeBox import Mathlib.RingTheory.Polynomial.Vieta import RealRooted.GraceHalfPlane import RealRooted.Multiaffine +import RealRooted.Mathlib.RingTheory.MvPolynomial.Symmetric import RealRooted.MultivariateStability /-! From eb4150cdbfbed5043b29c9ed7e487a2f9a20f85f Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Mon, 3 Aug 2026 10:20:37 +0000 Subject: [PATCH 24/81] Generalize symmetrization API --- .../RingTheory/MvPolynomial/Symmetric.lean | 22 ++++++++++--------- 1 file changed, 12 insertions(+), 10 deletions(-) diff --git a/RealRooted/Mathlib/RingTheory/MvPolynomial/Symmetric.lean b/RealRooted/Mathlib/RingTheory/MvPolynomial/Symmetric.lean index 35b7f5ca4..924bf4065 100644 --- a/RealRooted/Mathlib/RingTheory/MvPolynomial/Symmetric.lean +++ b/RealRooted/Mathlib/RingTheory/MvPolynomial/Symmetric.lean @@ -20,7 +20,7 @@ noncomputable def symmetrizationSum exact ∑ e : Equiv.Perm σ, rename e p /-- The permutation sum is symmetric. -/ -theorem isSymmetric_symmetrizationSum +theorem symmetrizationSum_isSymmetric {σ R : Type*} [Fintype σ] [CommSemiring R] (p : MvPolynomial σ R) : IsSymmetric (symmetrizationSum p) := by @@ -33,28 +33,30 @@ theorem isSymmetric_symmetrizationSum /-- Average all variable permutations of a complex multivariate polynomial. -/ noncomputable def fullSymmetrization - {σ : Type*} [Fintype σ] (p : MvPolynomial σ ℂ) : - MvPolynomial σ ℂ := by + {σ R : Type*} [Fintype σ] [Field R] [CharZero R] + (p : MvPolynomial σ R) : MvPolynomial σ R := by classical - exact C (Fintype.card (Equiv.Perm σ) : ℂ)⁻¹ * + exact C (Fintype.card (Equiv.Perm σ) : R)⁻¹ * symmetrizationSum p /-- Full symmetrization is symmetric. -/ -theorem isSymmetric_fullSymmetrization - {σ : Type*} [Fintype σ] (p : MvPolynomial σ ℂ) : +theorem fullSymmetrization_isSymmetric + {σ R : Type*} [Fintype σ] [Field R] [CharZero R] + (p : MvPolynomial σ R) : IsSymmetric (fullSymmetrization p) := by classical intro e simp only [fullSymmetrization, map_mul, rename_C] - rw [isSymmetric_symmetrizationSum p e] + rw [symmetrizationSum_isSymmetric p e] /-- Full symmetrization preserves evaluation at a constant assignment. -/ -theorem eval_const_fullSymmetrization - {σ : Type*} [Fintype σ] (p : MvPolynomial σ ℂ) (w : ℂ) : +theorem eval_fullSymmetrization_const + {σ R : Type*} [Fintype σ] [Field R] [CharZero R] + (p : MvPolynomial σ R) (w : R) : eval (fun _ : σ => w) (fullSymmetrization p) = eval (fun _ : σ => w) p := by classical - have hcard : (Fintype.card (Equiv.Perm σ) : ℂ) ≠ 0 := by + have hcard : (Fintype.card (Equiv.Perm σ) : R) ≠ 0 := by exact_mod_cast Fintype.card_ne_zero have hconst (e : Equiv.Perm σ) : (fun _ : σ => w) ∘ e = fun _ : σ => w := by From b418259f9c5fe3816728afc95472659bab63e85a Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Mon, 3 Aug 2026 10:29:59 +0000 Subject: [PATCH 25/81] Add partial polynomial symmetrization --- .../RingTheory/MvPolynomial/Symmetric.lean | 37 +++++++++++++++++++ RealRooted/Multiaffine.lean | 14 +++++++ RealRooted/Polarization.lean | 1 - 3 files changed, 51 insertions(+), 1 deletion(-) diff --git a/RealRooted/Mathlib/RingTheory/MvPolynomial/Symmetric.lean b/RealRooted/Mathlib/RingTheory/MvPolynomial/Symmetric.lean index 924bf4065..7e2cf911f 100644 --- a/RealRooted/Mathlib/RingTheory/MvPolynomial/Symmetric.lean +++ b/RealRooted/Mathlib/RingTheory/MvPolynomial/Symmetric.lean @@ -67,3 +67,40 @@ theorem eval_fullSymmetrization_const ← mul_assoc, inv_mul_cancel₀ hcard, one_mul] end MvPolynomial + +namespace MvPolynomial + +/-- Convex-form partial symmetrization associated with a permutation. -/ +noncomputable def partialSymmetrization + {σ R : Type*} [CommRing R] + (t : R) (e : Equiv.Perm σ) (p : MvPolynomial σ R) : + MvPolynomial σ R := + C t * p + C (1 - t) * rename e p + +/-- At weight zero, partial symmetrization is variable permutation. -/ +@[simp] theorem partialSymmetrization_zero + {σ R : Type*} [CommRing R] + (e : Equiv.Perm σ) (p : MvPolynomial σ R) : + partialSymmetrization 0 e p = rename e p := by + simp [partialSymmetrization] + +/-- At weight one, partial symmetrization is the original polynomial. -/ +@[simp] theorem partialSymmetrization_one + {σ R : Type*} [CommRing R] + (e : Equiv.Perm σ) (p : MvPolynomial σ R) : + partialSymmetrization 1 e p = p := by + simp [partialSymmetrization] + +/-- Partial symmetrization preserves evaluation at a constant assignment. -/ +theorem eval_partialSymmetrization_const + {σ R : Type*} [CommRing R] + (t w : R) (e : Equiv.Perm σ) (p : MvPolynomial σ R) : + eval (fun _ : σ => w) (partialSymmetrization t e p) = + eval (fun _ : σ => w) p := by + have hconst : (fun _ : σ => w) ∘ e = fun _ : σ => w := by + rfl + simp only [partialSymmetrization, map_add, map_mul, eval_C, + eval_rename, hconst] + ring + +end MvPolynomial diff --git a/RealRooted/Multiaffine.lean b/RealRooted/Multiaffine.lean index b86b863ed..d92a131a9 100644 --- a/RealRooted/Multiaffine.lean +++ b/RealRooted/Multiaffine.lean @@ -1,3 +1,4 @@ +import RealRooted.Mathlib.RingTheory.MvPolynomial.Symmetric import Mathlib.Algebra.MvPolynomial.PDeriv import Mathlib.RingTheory.MvPolynomial.Symmetric.Defs @@ -459,3 +460,16 @@ theorem esymm [Fintype σ] [Nontrivial R] (n : ℕ) : end IsMultiaffine end MvPolynomial + +namespace MvPolynomial + +/-- Partial symmetrization by a permutation preserves multiaffineness. -/ +theorem IsMultiaffine.partialSymmetrization + {σ R : Type*} [CommRing R] + {p : MvPolynomial σ R} (hp : IsMultiaffine p) + (t : R) (e : Equiv.Perm σ) : + IsMultiaffine (MvPolynomial.partialSymmetrization t e p) := by + exact (hp.C_mul t).add + ((hp.rename e.injective).C_mul (1 - t)) + +end MvPolynomial diff --git a/RealRooted/Polarization.lean b/RealRooted/Polarization.lean index da35ab062..59d412ad4 100644 --- a/RealRooted/Polarization.lean +++ b/RealRooted/Polarization.lean @@ -4,7 +4,6 @@ import RealRooted.Mathlib.Algebra.MvPolynomial.Stability.DegreeBox import Mathlib.RingTheory.Polynomial.Vieta import RealRooted.GraceHalfPlane import RealRooted.Multiaffine -import RealRooted.Mathlib.RingTheory.MvPolynomial.Symmetric import RealRooted.MultivariateStability /-! From 91e54b81b8b0d5df08653be9410ed0749399cd33 Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Mon, 3 Aug 2026 10:33:00 +0000 Subject: [PATCH 26/81] Prove partial symmetrization V-form identities --- RealRooted/PartialSymmetrization.lean | 46 +++++++++++++++++++++++++++ RealRooted/Polarization.lean | 2 +- 2 files changed, 47 insertions(+), 1 deletion(-) create mode 100644 RealRooted/PartialSymmetrization.lean diff --git a/RealRooted/PartialSymmetrization.lean b/RealRooted/PartialSymmetrization.lean new file mode 100644 index 000000000..9399522d0 --- /dev/null +++ b/RealRooted/PartialSymmetrization.lean @@ -0,0 +1,46 @@ +import RealRooted.Multiaffine + +/-! +# Partial symmetrization + +This file develops the bivariate coefficient identities used in the +Borcea--Brändén proof that transposition averages preserve stability. +-/ + +namespace RealRooted + +/-- The first real quadratic form from Borcea--Brändén, Part II, Lemma 1.4. -/ +def bivariateV1 (a b c d : ℂ) (x : ℝ) : ℝ := + (a * star c).im + (a * star d + b * star c).im * x + + (b * star d).im * x ^ 2 + +/-- The second real quadratic form from Borcea--Brändén, Part II, Lemma 1.4. -/ +def bivariateV2 (a b c d : ℂ) (x : ℝ) : ℝ := + (a * star b).im + (a * star d + c * star b).im * x + + (c * star d).im * x ^ 2 + +/-- Under partial transposition averaging, V1 is the corresponding convex +combination of the original V1 and V2. -/ +theorem bivariateV1_partialSymmetrization + (a b c d : ℂ) (t x : ℝ) : + bivariateV1 a + ((t : ℂ) * b + (1 - t : ℝ) * c) + ((t : ℂ) * c + (1 - t : ℝ) * b) d x = + t * bivariateV1 a b c d x + + (1 - t) * bivariateV2 a b c d x := by + simp [bivariateV1, bivariateV2, Complex.mul_im] + ring + +/-- Under partial transposition averaging, V2 is the corresponding convex +combination of the original V2 and V1. -/ +theorem bivariateV2_partialSymmetrization + (a b c d : ℂ) (t x : ℝ) : + bivariateV2 a + ((t : ℂ) * b + (1 - t : ℝ) * c) + ((t : ℂ) * c + (1 - t : ℝ) * b) d x = + t * bivariateV2 a b c d x + + (1 - t) * bivariateV1 a b c d x := by + simp [bivariateV1, bivariateV2, Complex.mul_im] + ring + +end RealRooted diff --git a/RealRooted/Polarization.lean b/RealRooted/Polarization.lean index 59d412ad4..f11ab88d5 100644 --- a/RealRooted/Polarization.lean +++ b/RealRooted/Polarization.lean @@ -3,7 +3,7 @@ import RealRooted.Mathlib.Algebra.MvPolynomial.Equiv import RealRooted.Mathlib.Algebra.MvPolynomial.Stability.DegreeBox import Mathlib.RingTheory.Polynomial.Vieta import RealRooted.GraceHalfPlane -import RealRooted.Multiaffine +import RealRooted.PartialSymmetrization import RealRooted.MultivariateStability /-! From d8ab820714a43c4103eacd814c41202c3e77b637 Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Mon, 3 Aug 2026 10:37:55 +0000 Subject: [PATCH 27/81] add degree-box modules to root imports --- RealRooted.lean | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/RealRooted.lean b/RealRooted.lean index 86b3c2b47..e119fd146 100644 --- a/RealRooted.lean +++ b/RealRooted.lean @@ -186,6 +186,8 @@ import RealRooted.LowerTriangularMatrix import RealRooted.MaWang import RealRooted.MagnitudeDominated import RealRooted.MaoWangMatrixProduct +import RealRooted.Mathlib.Algebra.MvPolynomial.Degrees +import RealRooted.Mathlib.Algebra.MvPolynomial.Equiv import RealRooted.Mathlib.Algebra.MvPolynomial.Stability.DegreeBox import RealRooted.Mathlib.Algebra.MvPolynomial.Stability.Symbol import RealRooted.Mathlib.Algebra.Polynomial.Basic @@ -207,6 +209,7 @@ import RealRooted.Mathlib.LinearAlgebra.Matrix.KernelSignVariation import RealRooted.Mathlib.LinearAlgebra.Matrix.SignVariation import RealRooted.Mathlib.LinearAlgebra.Matrix.TotallyNonneg import RealRooted.Mathlib.LinearAlgebra.Matrix.VariationDiminishing +import RealRooted.Mathlib.RingTheory.MvPolynomial.Symmetric import RealRooted.MatrixInterlacing import RealRooted.MultiaffineReciprocalRight import RealRooted.Multiaffine @@ -220,6 +223,7 @@ import RealRooted.ObreschkoffContinuity import RealRooted.ObreschkoffConverse import RealRooted.OperatorPreservesInterlacing import RealRooted.PFPolynomial +import RealRooted.PartialSymmetrization import RealRooted.Polarization import RealRooted.PolyaFrequencyConvolution import RealRooted.PosCombo From 1278c7530d7eca57a293d2c52b47b127faae9e32 Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Mon, 3 Aug 2026 10:47:48 +0000 Subject: [PATCH 28/81] add bivariate quotient boundary identities --- RealRooted/PartialSymmetrization.lean | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) diff --git a/RealRooted/PartialSymmetrization.lean b/RealRooted/PartialSymmetrization.lean index 9399522d0..c42133bd6 100644 --- a/RealRooted/PartialSymmetrization.lean +++ b/RealRooted/PartialSymmetrization.lean @@ -19,6 +19,26 @@ def bivariateV2 (a b c d : ℂ) (x : ℝ) : ℝ := (a * star b).im + (a * star d + c * star b).im * x + (c * star d).im * x ^ 2 +/-- The real-boundary quotient identity for `bivariateV1` from +Borcea--Brändén, Part II, Lemma 1.4. -/ +theorem im_bivariateQuotient_eq_bivariateV1_div_normSq + (a b c d : ℂ) (x : ℝ) : + ((a + b * (x : ℂ)) / (c + d * (x : ℂ))).im = + bivariateV1 a b c d x / + Complex.normSq (c + d * (x : ℂ)) := by + simp [Complex.div_im, Complex.normSq, bivariateV1] + ring + +/-- The symmetric real-boundary quotient identity for `bivariateV2` from +Borcea--Brändén, Part II, Lemma 1.4. -/ +theorem im_bivariateQuotient_eq_bivariateV2_div_normSq + (a b c d : ℂ) (x : ℝ) : + ((a + c * (x : ℂ)) / (b + d * (x : ℂ))).im = + bivariateV2 a b c d x / + Complex.normSq (b + d * (x : ℂ)) := by + simp [Complex.div_im, Complex.normSq, bivariateV2] + ring + /-- Under partial transposition averaging, V1 is the corresponding convex combination of the original V1 and V2. -/ theorem bivariateV1_partialSymmetrization From b6a379014900c1dd16658eb57e86eda87d27d642 Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Mon, 3 Aug 2026 10:49:59 +0000 Subject: [PATCH 29/81] add bivariate quotient positivity bridge --- RealRooted/PartialSymmetrization.lean | 38 +++++++++++++++++++++++++++ 1 file changed, 38 insertions(+) diff --git a/RealRooted/PartialSymmetrization.lean b/RealRooted/PartialSymmetrization.lean index c42133bd6..502455a31 100644 --- a/RealRooted/PartialSymmetrization.lean +++ b/RealRooted/PartialSymmetrization.lean @@ -39,6 +39,44 @@ theorem im_bivariateQuotient_eq_bivariateV2_div_normSq simp [Complex.div_im, Complex.normSq, bivariateV2] ring +/-- A positive imaginary part of `c / d` keeps `c + d * x` nonzero on the +real boundary. This is the denominator observation in Part II, Lemma 1.4. -/ +theorem add_mul_real_ne_zero_of_im_div_pos + (c d : ℂ) (x : ℝ) (h : 0 < (c / d).im) : + c + d * (x : ℂ) ≠ 0 := by + intro hzero + have hd : d ≠ 0 := by + intro hd + simp [hd] at h + have hratio : c / d = -(x : ℂ) := by + apply (div_eq_iff hd).2 + linear_combination hzero + rw [hratio] at h + simp at h + +/-- On the real boundary, positivity of the first quotient imaginary part is +equivalent to positivity of `bivariateV1` when its denominator stays off zero. -/ +theorem im_bivariateQuotient_pos_iff_bivariateV1_pos + (a b c d : ℂ) (x : ℝ) (h : 0 < (c / d).im) : + 0 < ((a + b * (x : ℂ)) / (c + d * (x : ℂ))).im ↔ + 0 < bivariateV1 a b c d x := by + have hden := add_mul_real_ne_zero_of_im_div_pos c d x h + have hnorm : 0 < Complex.normSq (c + d * (x : ℂ)) := + Complex.normSq_pos.mpr hden + rw [im_bivariateQuotient_eq_bivariateV1_div_normSq] + exact div_pos_iff_of_pos_right hnorm + +/-- The symmetric real-boundary positivity equivalence for `bivariateV2`. -/ +theorem im_bivariateQuotient_pos_iff_bivariateV2_pos + (a b c d : ℂ) (x : ℝ) (h : 0 < (b / d).im) : + 0 < ((a + c * (x : ℂ)) / (b + d * (x : ℂ))).im ↔ + 0 < bivariateV2 a b c d x := by + have hden := add_mul_real_ne_zero_of_im_div_pos b d x h + have hnorm : 0 < Complex.normSq (b + d * (x : ℂ)) := + Complex.normSq_pos.mpr hden + rw [im_bivariateQuotient_eq_bivariateV2_div_normSq] + exact div_pos_iff_of_pos_right hnorm + /-- Under partial transposition averaging, V1 is the corresponding convex combination of the original V1 and V2. -/ theorem bivariateV1_partialSymmetrization From 6a3b329ae06c6dd855ccf87b472614c5089a9d71 Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Mon, 3 Aug 2026 10:51:28 +0000 Subject: [PATCH 30/81] deduplicate symmetric bivariate proofs --- RealRooted/PartialSymmetrization.lean | 12 +++--------- 1 file changed, 3 insertions(+), 9 deletions(-) diff --git a/RealRooted/PartialSymmetrization.lean b/RealRooted/PartialSymmetrization.lean index 502455a31..3fd05b7e0 100644 --- a/RealRooted/PartialSymmetrization.lean +++ b/RealRooted/PartialSymmetrization.lean @@ -36,8 +36,7 @@ theorem im_bivariateQuotient_eq_bivariateV2_div_normSq ((a + c * (x : ℂ)) / (b + d * (x : ℂ))).im = bivariateV2 a b c d x / Complex.normSq (b + d * (x : ℂ)) := by - simp [Complex.div_im, Complex.normSq, bivariateV2] - ring + exact im_bivariateQuotient_eq_bivariateV1_div_normSq a c b d x /-- A positive imaginary part of `c / d` keeps `c + d * x` nonzero on the real boundary. This is the denominator observation in Part II, Lemma 1.4. -/ @@ -71,11 +70,7 @@ theorem im_bivariateQuotient_pos_iff_bivariateV2_pos (a b c d : ℂ) (x : ℝ) (h : 0 < (b / d).im) : 0 < ((a + c * (x : ℂ)) / (b + d * (x : ℂ))).im ↔ 0 < bivariateV2 a b c d x := by - have hden := add_mul_real_ne_zero_of_im_div_pos b d x h - have hnorm : 0 < Complex.normSq (b + d * (x : ℂ)) := - Complex.normSq_pos.mpr hden - rw [im_bivariateQuotient_eq_bivariateV2_div_normSq] - exact div_pos_iff_of_pos_right hnorm + exact im_bivariateQuotient_pos_iff_bivariateV1_pos a c b d x h /-- Under partial transposition averaging, V1 is the corresponding convex combination of the original V1 and V2. -/ @@ -98,7 +93,6 @@ theorem bivariateV2_partialSymmetrization ((t : ℂ) * c + (1 - t : ℝ) * b) d x = t * bivariateV2 a b c d x + (1 - t) * bivariateV1 a b c d x := by - simp [bivariateV1, bivariateV2, Complex.mul_im] - ring + exact bivariateV1_partialSymmetrization a c b d t x end RealRooted From 8dba4c672b1d8e3046d76f35574e0cd0f87597ae Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Mon, 3 Aug 2026 10:54:05 +0000 Subject: [PATCH 31/81] formalize bivariate solve-for-variable step --- RealRooted/PartialSymmetrization.lean | 45 +++++++++++++++++++++++---- 1 file changed, 39 insertions(+), 6 deletions(-) diff --git a/RealRooted/PartialSymmetrization.lean b/RealRooted/PartialSymmetrization.lean index 3fd05b7e0..6f6520e14 100644 --- a/RealRooted/PartialSymmetrization.lean +++ b/RealRooted/PartialSymmetrization.lean @@ -38,20 +38,53 @@ theorem im_bivariateQuotient_eq_bivariateV2_div_normSq Complex.normSq (b + d * (x : ℂ)) := by exact im_bivariateQuotient_eq_bivariateV1_div_normSq a c b d x -/-- A positive imaginary part of `c / d` keeps `c + d * x` nonzero on the -real boundary. This is the denominator observation in Part II, Lemma 1.4. -/ -theorem add_mul_real_ne_zero_of_im_div_pos - (c d : ℂ) (x : ℝ) (h : 0 < (c / d).im) : - c + d * (x : ℂ) ≠ 0 := by +/-- A positive imaginary part of `c / d` keeps `c + d * z` nonzero on the +closed upper half-plane. This is the denominator observation in Part II, +Lemma 1.4. -/ +theorem add_mul_ne_zero_of_im_div_pos + (c d z : ℂ) (h : 0 < (c / d).im) (hz : 0 ≤ z.im) : + c + d * z ≠ 0 := by intro hzero have hd : d ≠ 0 := by intro hd simp [hd] at h - have hratio : c / d = -(x : ℂ) := by + have hratio : c / d = -z := by apply (div_eq_iff hd).2 linear_combination hzero rw [hratio] at h simp at h + linarith + +/-- The real-boundary specialization of +`add_mul_ne_zero_of_im_div_pos`. -/ +theorem add_mul_real_ne_zero_of_im_div_pos + (c d : ℂ) (x : ℝ) (h : 0 < (c / d).im) : + c + d * (x : ℂ) ≠ 0 := by + exact add_mul_ne_zero_of_im_div_pos c d x h (by simp) + +/-- Solving a bivariate multiaffine expression for its second variable, as in +the proof of Borcea--Brändén, Part II, Lemma 1.4. -/ +theorem bivariate_eq_factor_quotient + (a b c d z w : ℂ) (hden : c + d * z ≠ 0) : + a + b * z + c * w + d * z * w = + (c + d * z) * (w + (a + b * z) / (c + d * z)) := by + calc + a + b * z + c * w + d * z * w = + (c + d * z) * w + (a + b * z) := by ring + _ = (c + d * z) * w + + (c + d * z) * ((a + b * z) / (c + d * z)) := by + rw [mul_div_cancel₀ (a + b * z) hden] + _ = (c + d * z) * (w + (a + b * z) / (c + d * z)) := by ring + +/-- With a nonzero denominator, the bivariate expression has the unique +second-variable zero used in equation (1.2) of Part II. -/ +theorem bivariate_eq_zero_iff + (a b c d z w : ℂ) (hden : c + d * z ≠ 0) : + a + b * z + c * w + d * z * w = 0 ↔ + w = -((a + b * z) / (c + d * z)) := by + rw [bivariate_eq_factor_quotient a b c d z w hden] + simp only [mul_eq_zero, hden, false_or] + constructor <;> intro h <;> linear_combination h /-- On the real boundary, positivity of the first quotient imaginary part is equivalent to positivity of `bivariateV1` when its denominator stays off zero. -/ From c3d8a0b15ed4aeff3106151a0b701f901ced63af Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Mon, 3 Aug 2026 10:58:38 +0000 Subject: [PATCH 32/81] derive bivariate nonvanishing from quotient positivity --- RealRooted/PartialSymmetrization.lean | 21 +++++++++++++++++++++ 1 file changed, 21 insertions(+) diff --git a/RealRooted/PartialSymmetrization.lean b/RealRooted/PartialSymmetrization.lean index 6f6520e14..0588ffd30 100644 --- a/RealRooted/PartialSymmetrization.lean +++ b/RealRooted/PartialSymmetrization.lean @@ -86,6 +86,27 @@ theorem bivariate_eq_zero_iff simp only [mul_eq_zero, hden, false_or] constructor <;> intro h <;> linear_combination h +/-- Positive imaginary part of the solved quotient excludes a zero with the +second variable in the upper half-plane. -/ +theorem bivariate_ne_zero_of_quotient_im_pos + (a b c d z w : ℂ) (hden : c + d * z ≠ 0) + (hq : 0 < ((a + b * z) / (c + d * z)).im) (hw : 0 < w.im) : + a + b * z + c * w + d * z * w ≠ 0 := by + intro hzero + have hroot := (bivariate_eq_zero_iff a b c d z w hden).mp hzero + rw [hroot] at hw + simp at hw + linarith + +/-- The source's quotient-positivity condition implies bivariate nonvanishing +on the upper half-plane. This is the algebraic direction preceding (1.2). -/ +theorem bivariate_ne_zero_of_im_div_pos_of_quotient_im_pos + (a b c d z w : ℂ) (hcd : 0 < (c / d).im) (hz : 0 ≤ z.im) + (hq : 0 < ((a + b * z) / (c + d * z)).im) (hw : 0 < w.im) : + a + b * z + c * w + d * z * w ≠ 0 := by + exact bivariate_ne_zero_of_quotient_im_pos a b c d z w + (add_mul_ne_zero_of_im_div_pos c d z hcd hz) hq hw + /-- On the real boundary, positivity of the first quotient imaginary part is equivalent to positivity of `bivariateV1` when its denominator stays off zero. -/ theorem im_bivariateQuotient_pos_iff_bivariateV1_pos From 24ed20acd2edd0108846a553b5510964071ece24 Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Mon, 3 Aug 2026 10:59:58 +0000 Subject: [PATCH 33/81] define second bivariate form by symmetry --- RealRooted/PartialSymmetrization.lean | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/RealRooted/PartialSymmetrization.lean b/RealRooted/PartialSymmetrization.lean index 0588ffd30..35f1acaf5 100644 --- a/RealRooted/PartialSymmetrization.lean +++ b/RealRooted/PartialSymmetrization.lean @@ -16,8 +16,7 @@ def bivariateV1 (a b c d : ℂ) (x : ℝ) : ℝ := /-- The second real quadratic form from Borcea--Brändén, Part II, Lemma 1.4. -/ def bivariateV2 (a b c d : ℂ) (x : ℝ) : ℝ := - (a * star b).im + (a * star d + c * star b).im * x + - (c * star d).im * x ^ 2 + bivariateV1 a c b d x /-- The real-boundary quotient identity for `bivariateV1` from Borcea--Brändén, Part II, Lemma 1.4. -/ From b08fdf104de4cab22f2a9910e34623917958c440 Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Mon, 3 Aug 2026 11:03:03 +0000 Subject: [PATCH 34/81] bridge bivariate quotient criterion to stability --- RealRooted/PartialSymmetrization.lean | 27 +++++++++++++++++++++++++++ 1 file changed, 27 insertions(+) diff --git a/RealRooted/PartialSymmetrization.lean b/RealRooted/PartialSymmetrization.lean index 35f1acaf5..cc69210b5 100644 --- a/RealRooted/PartialSymmetrization.lean +++ b/RealRooted/PartialSymmetrization.lean @@ -9,6 +9,8 @@ Borcea--Brändén proof that transposition averages preserve stability. namespace RealRooted +open MvPolynomial + /-- The first real quadratic form from Borcea--Brändén, Part II, Lemma 1.4. -/ def bivariateV1 (a b c d : ℂ) (x : ℝ) : ℝ := (a * star c).im + (a * star d + b * star c).im * x + @@ -18,6 +20,19 @@ def bivariateV1 (a b c d : ℂ) (x : ℝ) : ℝ := def bivariateV2 (a b c d : ℂ) (x : ℝ) : ℝ := bivariateV1 a c b d x +/-- The four-coefficient bivariate multiaffine polynomial used in Part II, +Lemma 1.4. -/ +noncomputable def bivariateMultiaffinePolynomial (a b c d : ℂ) : + MvPolynomial (Fin 2) ℂ := + C a + C b * X 0 + C c * X 1 + C d * X 0 * X 1 + +/-- Evaluation of the four-coefficient bivariate multiaffine polynomial. -/ +theorem eval_bivariateMultiaffinePolynomial + (a b c d : ℂ) (z : Fin 2 → ℂ) : + MvPolynomial.eval z (bivariateMultiaffinePolynomial a b c d) = + a + b * z 0 + c * z 1 + d * z 0 * z 1 := by + simp [bivariateMultiaffinePolynomial] + /-- The real-boundary quotient identity for `bivariateV1` from Borcea--Brändén, Part II, Lemma 1.4. -/ theorem im_bivariateQuotient_eq_bivariateV1_div_normSq @@ -106,6 +121,18 @@ theorem bivariate_ne_zero_of_im_div_pos_of_quotient_im_pos exact bivariate_ne_zero_of_quotient_im_pos a b c d z w (add_mul_ne_zero_of_im_div_pos c d z hcd hz) hq hw +/-- The quotient-positivity condition in (1.2) implies upper-half-plane +stability of the corresponding bivariate multiaffine polynomial. -/ +theorem mvUpperHalfPlaneStable_bivariate_of_quotient_im_pos + (a b c d : ℂ) (hcd : 0 < (c / d).im) + (hq : ∀ z : ℂ, 0 < z.im → + 0 < ((a + b * z) / (c + d * z)).im) : + MvUpperHalfPlaneStable (bivariateMultiaffinePolynomial a b c d) := by + intro z hz + rw [eval_bivariateMultiaffinePolynomial] + exact bivariate_ne_zero_of_im_div_pos_of_quotient_im_pos + a b c d (z 0) (z 1) hcd (le_of_lt (hz 0)) (hq (z 0) (hz 0)) (hz 1) + /-- On the real boundary, positivity of the first quotient imaginary part is equivalent to positivity of `bivariateV1` when its denominator stays off zero. -/ theorem im_bivariateQuotient_pos_iff_bivariateV1_pos From 68bfea4c44e2a05b03bb15943b6032b9f011cf08 Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Mon, 3 Aug 2026 11:09:48 +0000 Subject: [PATCH 35/81] derive weak quotient positivity from stability --- RealRooted/PartialSymmetrization.lean | 24 ++++++++++++++++++++++++ 1 file changed, 24 insertions(+) diff --git a/RealRooted/PartialSymmetrization.lean b/RealRooted/PartialSymmetrization.lean index cc69210b5..10e1a437a 100644 --- a/RealRooted/PartialSymmetrization.lean +++ b/RealRooted/PartialSymmetrization.lean @@ -133,6 +133,30 @@ theorem mvUpperHalfPlaneStable_bivariate_of_quotient_im_pos exact bivariate_ne_zero_of_im_div_pos_of_quotient_im_pos a b c d (z 0) (z 1) hcd (le_of_lt (hz 0)) (hq (z 0) (hz 0)) (hz 1) +/-- Stability forces the solved quotient into the closed upper half-plane. +Upgrading this weak inequality to strict positivity is the separate +open-mapping step in the proof of Part II, Lemma 1.4. -/ +theorem quotient_im_nonneg_of_mvUpperHalfPlaneStable_bivariate + (a b c d : ℂ) + (hP : MvUpperHalfPlaneStable (bivariateMultiaffinePolynomial a b c d)) + (hcd : 0 < (c / d).im) (z : ℂ) (hz : 0 < z.im) : + 0 ≤ ((a + b * z) / (c + d * z)).im := by + by_contra hq + let w := -((a + b * z) / (c + d * z)) + have hw : 0 < w.im := by + dsimp [w] + simp + linarith + have hstable := hP ![z, w] (by + intro i + fin_cases i + · simpa using hz + · simpa using hw) + rw [eval_bivariateMultiaffinePolynomial] at hstable + apply hstable + exact (bivariate_eq_zero_iff a b c d z w + (add_mul_ne_zero_of_im_div_pos c d z hcd (le_of_lt hz))).2 rfl + /-- On the real boundary, positivity of the first quotient imaginary part is equivalent to positivity of `bivariateV1` when its denominator stays off zero. -/ theorem im_bivariateQuotient_pos_iff_bivariateV1_pos From 33979985a3c7e40532b49b0be597d4acd8d83e12 Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Mon, 3 Aug 2026 11:11:54 +0000 Subject: [PATCH 36/81] golf bivariate weak converse proof --- RealRooted/PartialSymmetrization.lean | 9 +++------ 1 file changed, 3 insertions(+), 6 deletions(-) diff --git a/RealRooted/PartialSymmetrization.lean b/RealRooted/PartialSymmetrization.lean index 10e1a437a..242788dae 100644 --- a/RealRooted/PartialSymmetrization.lean +++ b/RealRooted/PartialSymmetrization.lean @@ -149,13 +149,10 @@ theorem quotient_im_nonneg_of_mvUpperHalfPlaneStable_bivariate linarith have hstable := hP ![z, w] (by intro i - fin_cases i - · simpa using hz - · simpa using hw) + fin_cases i <;> simp_all) rw [eval_bivariateMultiaffinePolynomial] at hstable - apply hstable - exact (bivariate_eq_zero_iff a b c d z w - (add_mul_ne_zero_of_im_div_pos c d z hcd (le_of_lt hz))).2 rfl + exact hstable ((bivariate_eq_zero_iff a b c d z w + (add_mul_ne_zero_of_im_div_pos c d z hcd (le_of_lt hz))).2 rfl) /-- On the real boundary, positivity of the first quotient imaginary part is equivalent to positivity of `bivariateV1` when its denominator stays off zero. -/ From 1c34decd008d7f20a3e8d6d615cc82f2dc469caa Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Mon, 3 Aug 2026 11:13:27 +0000 Subject: [PATCH 37/81] formalize constant bivariate quotient branch --- RealRooted/PartialSymmetrization.lean | 24 ++++++++++++++++++++++++ 1 file changed, 24 insertions(+) diff --git a/RealRooted/PartialSymmetrization.lean b/RealRooted/PartialSymmetrization.lean index 242788dae..ddefd1746 100644 --- a/RealRooted/PartialSymmetrization.lean +++ b/RealRooted/PartialSymmetrization.lean @@ -76,6 +76,30 @@ theorem add_mul_real_ne_zero_of_im_div_pos c + d * (x : ℂ) ≠ 0 := by exact add_mul_ne_zero_of_im_div_pos c d x h (by simp) +/-- When the cross determinant vanishes, the solved quotient is the constant +`b / d`. This is the constant branch in Part II, Lemma 1.4. -/ +theorem bivariateQuotient_eq_b_div + (a b c d z : ℂ) (hcross : a * d = b * c) + (hd : d ≠ 0) (hden : c + d * z ≠ 0) : + (a + b * z) / (c + d * z) = b / d := by + apply (div_eq_iff hden).2 + field_simp [hd] + linear_combination hcross + +/-- In the constant branch, positivity at infinity gives strict quotient +positivity throughout the closed upper half-plane. -/ +theorem bivariateQuotient_im_pos_of_cross_eq + (a b c d z : ℂ) (hcross : a * d = b * c) + (hbd : 0 < (b / d).im) (hcd : 0 < (c / d).im) + (hz : 0 ≤ z.im) : + 0 < ((a + b * z) / (c + d * z)).im := by + have hd : d ≠ 0 := by + intro hd + simp [hd] at hbd + rw [bivariateQuotient_eq_b_div a b c d z hcross hd + (add_mul_ne_zero_of_im_div_pos c d z hcd hz)] + exact hbd + /-- Solving a bivariate multiaffine expression for its second variable, as in the proof of Borcea--Brändén, Part II, Lemma 1.4. -/ theorem bivariate_eq_factor_quotient From f9a9215baa69f2134c92365e2cb30c9ce52e9d81 Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Mon, 3 Aug 2026 11:15:19 +0000 Subject: [PATCH 38/81] add nonconstant bivariate quotient witness --- RealRooted/PartialSymmetrization.lean | 24 ++++++++++++++++++++++++ 1 file changed, 24 insertions(+) diff --git a/RealRooted/PartialSymmetrization.lean b/RealRooted/PartialSymmetrization.lean index ddefd1746..d1e6358dd 100644 --- a/RealRooted/PartialSymmetrization.lean +++ b/RealRooted/PartialSymmetrization.lean @@ -100,6 +100,30 @@ theorem bivariateQuotient_im_pos_of_cross_eq (add_mul_ne_zero_of_im_div_pos c d z hcd hz)] exact hbd +/-- A nonzero cross determinant makes the quotient take different values at +`z` and `z + 1`, provided both denominators are nonzero. -/ +theorem bivariateQuotient_ne_add_one + (a b c d z : ℂ) (hcross : a * d ≠ b * c) + (hden : c + d * z ≠ 0) (hden1 : c + d * (z + 1) ≠ 0) : + (a + b * z) / (c + d * z) ≠ + (a + b * (z + 1)) / (c + d * (z + 1)) := by + intro heq + have hmul := (div_eq_div_iff hden hden1).mp heq + apply hcross + linear_combination hmul + +/-- Under the denominator half-plane hypothesis, a nonzero cross determinant +gives an explicit nonconstancy witness within the same closed half-plane. -/ +theorem bivariateQuotient_ne_add_one_of_im_div_pos + (a b c d z : ℂ) (hcross : a * d ≠ b * c) + (hcd : 0 < (c / d).im) (hz : 0 ≤ z.im) : + (a + b * z) / (c + d * z) ≠ + (a + b * (z + 1)) / (c + d * (z + 1)) := by + apply bivariateQuotient_ne_add_one a b c d z hcross + · exact add_mul_ne_zero_of_im_div_pos c d z hcd hz + · apply add_mul_ne_zero_of_im_div_pos c d (z + 1) hcd + simpa using hz + /-- Solving a bivariate multiaffine expression for its second variable, as in the proof of Borcea--Brändén, Part II, Lemma 1.4. -/ theorem bivariate_eq_factor_quotient From 8862136b85d7f0030e6422a2ad9e6ccca7133acf Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Mon, 3 Aug 2026 11:16:30 +0000 Subject: [PATCH 39/81] deduplicate quotient denominator proofs --- RealRooted/PartialSymmetrization.lean | 18 +++++++++++------- 1 file changed, 11 insertions(+), 7 deletions(-) diff --git a/RealRooted/PartialSymmetrization.lean b/RealRooted/PartialSymmetrization.lean index d1e6358dd..357fbb57e 100644 --- a/RealRooted/PartialSymmetrization.lean +++ b/RealRooted/PartialSymmetrization.lean @@ -52,6 +52,14 @@ theorem im_bivariateQuotient_eq_bivariateV2_div_normSq Complex.normSq (b + d * (x : ℂ)) := by exact im_bivariateQuotient_eq_bivariateV1_div_normSq a c b d x +/-- A positive imaginary part of `c / d` keeps `c + d * z` nonzero on the +closed upper half-plane. This is the denominator observation in Part II, +Lemma 1.4. -/ +theorem right_ne_zero_of_im_div_pos + (c d : ℂ) (h : 0 < (c / d).im) : d ≠ 0 := by + intro hd + simp [hd] at h + /-- A positive imaginary part of `c / d` keeps `c + d * z` nonzero on the closed upper half-plane. This is the denominator observation in Part II, Lemma 1.4. -/ @@ -59,9 +67,7 @@ theorem add_mul_ne_zero_of_im_div_pos (c d z : ℂ) (h : 0 < (c / d).im) (hz : 0 ≤ z.im) : c + d * z ≠ 0 := by intro hzero - have hd : d ≠ 0 := by - intro hd - simp [hd] at h + have hd := right_ne_zero_of_im_div_pos c d h have hratio : c / d = -z := by apply (div_eq_iff hd).2 linear_combination hzero @@ -93,10 +99,8 @@ theorem bivariateQuotient_im_pos_of_cross_eq (hbd : 0 < (b / d).im) (hcd : 0 < (c / d).im) (hz : 0 ≤ z.im) : 0 < ((a + b * z) / (c + d * z)).im := by - have hd : d ≠ 0 := by - intro hd - simp [hd] at hbd - rw [bivariateQuotient_eq_b_div a b c d z hcross hd + rw [bivariateQuotient_eq_b_div a b c d z hcross + (right_ne_zero_of_im_div_pos b d hbd) (add_mul_ne_zero_of_im_div_pos c d z hcd hz)] exact hbd From a3e25db51446412de07b6ab96662a61b27c25aca Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Mon, 3 Aug 2026 11:19:18 +0000 Subject: [PATCH 40/81] add analytic upper-half-plane strictness lemma --- .../Mathlib/Analysis/Complex/OpenMapping.lean | 35 ++++++++++++++++++- 1 file changed, 34 insertions(+), 1 deletion(-) diff --git a/RealRooted/Mathlib/Analysis/Complex/OpenMapping.lean b/RealRooted/Mathlib/Analysis/Complex/OpenMapping.lean index 72dbc48ca..5866a23ec 100644 --- a/RealRooted/Mathlib/Analysis/Complex/OpenMapping.lean +++ b/RealRooted/Mathlib/Analysis/Complex/OpenMapping.lean @@ -1,7 +1,7 @@ import Mathlib.Analysis.Complex.OpenMapping /-! -# Complex polynomial consequences of the open mapping theorem +# Complex consequences of the open mapping theorem This file contains general-purpose compatibility lemmas intended for eventual upstreaming to Mathlib. @@ -12,6 +12,39 @@ open scoped Topology noncomputable section +namespace AnalyticAt + +/-- A locally nonconstant analytic map that is eventually confined to the +closed upper half-plane takes its base point into the open upper half-plane. -/ +theorem im_pos_of_eventually_im_nonneg + {f : ℂ → ℂ} {z₀ : ℂ} (hf : AnalyticAt ℂ f z₀) + (hnotconst : ¬∀ᶠ z in 𝓝 z₀, f z = f z₀) + (hzero : 0 ≤ (f z₀).im) + (hnonneg : ∀ᶠ z in 𝓝 z₀, 0 ≤ (f z).im) : + 0 < (f z₀).im := by + by_contra hpos + have himzero : (f z₀).im = 0 := + le_antisymm (le_of_not_gt hpos) hzero + have hmap : 𝓝 (f z₀) ≤ Filter.map f (𝓝 z₀) := + hf.eventually_constant_or_nhds_le_map_nhds_aux.resolve_left hnotconst + have himage : f '' {z | 0 ≤ (f z).im} ∈ 𝓝 (f z₀) := + hmap (image_mem_map hnonneg) + obtain ⟨ε, hε, hball⟩ := Metric.mem_nhds_iff.mp himage + let w : ℂ := f z₀ - (ε / 2 : ℝ) * Complex.I + have hwball : w ∈ ball (f z₀) ε := by + rw [mem_ball] + simp [w, Real.norm_eq_abs, abs_of_pos hε] + linarith + have hwim : w.im < 0 := by + simp [w, himzero] + linarith + obtain ⟨z, hz, hzw⟩ := hball hwball + change 0 ≤ (f z).im at hz + rw [hzw] at hz + linarith + +end AnalyticAt + namespace Polynomial private theorem neg_eval_div_eval_image_mem_nhds From ae59cde682743150a570f64f0b53603aa9b7f277 Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Mon, 3 Aug 2026 11:22:14 +0000 Subject: [PATCH 41/81] import upstream iterated derivative tactic modules --- RealRooted.lean | 2 ++ 1 file changed, 2 insertions(+) diff --git a/RealRooted.lean b/RealRooted.lean index e119fd146..ba00cd36c 100644 --- a/RealRooted.lean +++ b/RealRooted.lean @@ -293,6 +293,7 @@ import RealRooted.Tactic.Examples.HomogenizeStable import RealRooted.Tactic.Examples.I2DerivativeLag import RealRooted.Tactic.Examples.InterlacingSequence import RealRooted.Tactic.Examples.IteratedDerivativeShift +import RealRooted.Tactic.Examples.IteratedDerivativeShiftProduct import RealRooted.Tactic.Examples.J1Chebyshev import RealRooted.Tactic.Examples.J1Gap3Reciprocal import RealRooted.Tactic.Examples.Kurtz @@ -341,6 +342,7 @@ import RealRooted.Tactic.HomogenizeStable import RealRooted.Tactic.I2DerivativeLag import RealRooted.Tactic.InterlacingSequence import RealRooted.Tactic.IteratedDerivativeShift +import RealRooted.Tactic.IteratedDerivativeShiftProduct import RealRooted.Tactic.J1Chebyshev import RealRooted.Tactic.J1Gap3Reciprocal import RealRooted.Tactic.Kurtz From aace948ab10e2a97f328227ce963f382e5d024f5 Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Mon, 3 Aug 2026 11:26:04 +0000 Subject: [PATCH 42/81] add bivariate quotient local nonconstancy --- RealRooted.lean | 1 + RealRooted/BivariateOpenMapping.lean | 59 ++++++++++++++++++++++++++++ 2 files changed, 60 insertions(+) create mode 100644 RealRooted/BivariateOpenMapping.lean diff --git a/RealRooted.lean b/RealRooted.lean index ba00cd36c..b344b2a01 100644 --- a/RealRooted.lean +++ b/RealRooted.lean @@ -21,6 +21,7 @@ import RealRooted.AllCombo import RealRooted.Apolarity import RealRooted.Basic import RealRooted.Bezoutian +import RealRooted.BivariateOpenMapping import RealRooted.BoundarySpecializationRight import RealRooted.BorceaBranden.BoundarySpecialization import RealRooted.BorceaBranden.FiniteSymbolCoefficient diff --git a/RealRooted/BivariateOpenMapping.lean b/RealRooted/BivariateOpenMapping.lean new file mode 100644 index 000000000..0b5345e1f --- /dev/null +++ b/RealRooted/BivariateOpenMapping.lean @@ -0,0 +1,59 @@ +import RealRooted.Mathlib.Analysis.Complex.OpenMapping +import RealRooted.PartialSymmetrization + +/-! +# Open mapping for bivariate multiaffine quotients + +This file supplies the local nonconstancy input for the open-mapping step in +Borcea--Brändén, Part II, Lemma 1.4. +-/ + +open Filter Metric Set +open scoped Topology + +namespace RealRooted + +/-- A nonzero cross determinant makes the bivariate quotient injective wherever +both denominators are nonzero. -/ +theorem bivariateQuotient_ne_of_ne + (a b c d z t : ℂ) (hcross : a * d ≠ b * c) + (hdenz : c + d * z ≠ 0) (hdent : c + d * t ≠ 0) (hzt : z ≠ t) : + (a + b * z) / (c + d * z) ≠ + (a + b * t) / (c + d * t) := by + intro heq + have hmul := (div_eq_div_iff hdenz hdent).mp heq + have hzero : (a * d - b * c) * (t - z) = 0 := by + linear_combination hmul + exact (mul_ne_zero (sub_ne_zero.mpr hcross) + (sub_ne_zero.mpr hzt.symm)) hzero + +/-- Under the denominator half-plane hypothesis, a nonzero cross determinant +rules out local eventual constancy of the bivariate quotient. -/ +theorem bivariateQuotient_not_eventually_constant + (a b c d z : ℂ) (hcross : a * d ≠ b * c) + (hcd : 0 < (c / d).im) (hz : 0 < z.im) : + ¬∀ᶠ t in 𝓝 z, + (a + b * t) / (c + d * t) = (a + b * z) / (c + d * z) := by + intro hconst + obtain ⟨ε, hε, hball⟩ := Metric.mem_nhds_iff.mp hconst + let t : ℂ := z + (ε / 2 : ℝ) + have htball : t ∈ ball z ε := by + rw [mem_ball] + simp [t, Real.norm_eq_abs, abs_of_pos hε] + linarith + have heq := hball htball + have htne : z ≠ t := by + intro heq' + have hre := congrArg Complex.re heq' + simp [t] at hre + linarith + apply bivariateQuotient_ne_of_ne a b c d z t hcross + · exact add_mul_ne_zero_of_im_div_pos c d z hcd (le_of_lt hz) + · apply add_mul_ne_zero_of_im_div_pos c d t hcd + simpa only [t, Complex.add_im, Complex.ofReal_im, add_zero] using le_of_lt hz + · exact htne + · change (a + b * t) / (c + d * t) = + (a + b * z) / (c + d * z) at heq + exact heq.symm + +end RealRooted From 782d9185255a709cd7a0fa160ca75db12a7063a2 Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Mon, 3 Aug 2026 13:36:39 +0000 Subject: [PATCH 43/81] Repair degree-box comparator blockers --- RealRooted/BivariateOpenMapping.lean | 16 ++++++++-------- .../Algebra/MvPolynomial/Stability/Symbol.lean | 3 +-- .../RingTheory/MvPolynomial/Symmetric.lean | 5 +++++ 3 files changed, 14 insertions(+), 10 deletions(-) diff --git a/RealRooted/BivariateOpenMapping.lean b/RealRooted/BivariateOpenMapping.lean index 0b5345e1f..d1a2271ca 100644 --- a/RealRooted/BivariateOpenMapping.lean +++ b/RealRooted/BivariateOpenMapping.lean @@ -47,13 +47,13 @@ theorem bivariateQuotient_not_eventually_constant have hre := congrArg Complex.re heq' simp [t] at hre linarith - apply bivariateQuotient_ne_of_ne a b c d z t hcross - · exact add_mul_ne_zero_of_im_div_pos c d z hcd (le_of_lt hz) - · apply add_mul_ne_zero_of_im_div_pos c d t hcd - simpa only [t, Complex.add_im, Complex.ofReal_im, add_zero] using le_of_lt hz - · exact htne - · change (a + b * t) / (c + d * t) = - (a + b * z) / (c + d * z) at heq - exact heq.symm + change (a + b * t) / (c + d * t) = + (a + b * z) / (c + d * z) at heq + have hdent : c + d * t ≠ 0 := + add_mul_ne_zero_of_im_div_pos c d t hcd (by + simpa only [t, Complex.add_im, Complex.ofReal_im, add_zero] using le_of_lt hz) + exact bivariateQuotient_ne_of_ne a b c d z t hcross + (add_mul_ne_zero_of_im_div_pos c d z hcd (le_of_lt hz)) + hdent htne heq.symm end RealRooted diff --git a/RealRooted/Mathlib/Algebra/MvPolynomial/Stability/Symbol.lean b/RealRooted/Mathlib/Algebra/MvPolynomial/Stability/Symbol.lean index aa874e25a..a8d4441cd 100644 --- a/RealRooted/Mathlib/Algebra/MvPolynomial/Stability/Symbol.lean +++ b/RealRooted/Mathlib/Algebra/MvPolynomial/Stability/Symbol.lean @@ -48,8 +48,7 @@ theorem boxChoose_one_of_le_one (m : σ →₀ ℕ) (hm : ∀ i, m i ≤ 1) : simp only [boxChoose] apply Finset.prod_eq_one intro i hi - have hle := hm i - interval_cases h : m i <;> simp + rcases Nat.le_one_iff_eq_zero_or_eq_one.mp (hm i) with h | h <;> simp [h] /-- The right-block monomial with exponent vector `κ - m`. -/ noncomputable def rightComplementMonomial (κ : σ → ℕ) (m : σ →₀ ℕ) : diff --git a/RealRooted/Mathlib/RingTheory/MvPolynomial/Symmetric.lean b/RealRooted/Mathlib/RingTheory/MvPolynomial/Symmetric.lean index 7e2cf911f..1ad97ec57 100644 --- a/RealRooted/Mathlib/RingTheory/MvPolynomial/Symmetric.lean +++ b/RealRooted/Mathlib/RingTheory/MvPolynomial/Symmetric.lean @@ -12,6 +12,11 @@ open BigOperators namespace MvPolynomial +/-- The finite indexing type of permutations induced by a finite type. -/ +noncomputable local instance {σ : Type*} [Fintype σ] : + Fintype (Equiv.Perm σ) := + Fintype.ofFinite _ + /-- Sum all variable permutations of a multivariate polynomial. -/ noncomputable def symmetrizationSum {σ R : Type*} [Fintype σ] [CommSemiring R] From 6e2df3de9880f5a992b3c9f3af9fda2e4bd6fcc3 Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Mon, 3 Aug 2026 20:09:06 +0000 Subject: [PATCH 44/81] Repair finite-symbol dependency imports --- RealRooted/BorceaBranden/FiniteSymbolBasis.lean | 10 ++++++---- RealRooted/PartialSymmetrization.lean | 1 + 2 files changed, 7 insertions(+), 4 deletions(-) diff --git a/RealRooted/BorceaBranden/FiniteSymbolBasis.lean b/RealRooted/BorceaBranden/FiniteSymbolBasis.lean index 66815b4d8..204d192e3 100644 --- a/RealRooted/BorceaBranden/FiniteSymbolBasis.lean +++ b/RealRooted/BorceaBranden/FiniteSymbolBasis.lean @@ -1,5 +1,6 @@ +import Mathlib.Data.Finsupp.Weight import RealRooted.BorceaBranden.FiniteSymbolCoefficient -import RealRooted.Mathlib.Algebra.MvPolynomial.Stability.DegreeBox +import RealRooted.Mathlib.Algebra.MvPolynomial.Stability.Symbol /-! # Degree-one exponent coordinates for finite symbols @@ -21,8 +22,8 @@ theorem finsupp_eq_indicator_support_of_le_one d = Finsupp.indicator d.support (fun _ _ => 1) := by classical ext i - have hle := hd i - interval_cases h : d i <;> simp [Finsupp.indicator, h] + rcases Nat.le_one_iff_eq_zero_or_eq_one.mp (hd i) with h | h <;> + simp [Finsupp.indicator, h] /-- Coordinate-wise degree-one exponent vectors are equal exactly when their supports are equal. -/ @@ -97,7 +98,8 @@ namespace Finsupp simpa [mem_support_iff] using hi apply Finsupp.ext intro i - fin_cases i + have hi : i = 0 := Fin.eq_zero i + subst i rw [hdegree] simp diff --git a/RealRooted/PartialSymmetrization.lean b/RealRooted/PartialSymmetrization.lean index 357fbb57e..111fda0f4 100644 --- a/RealRooted/PartialSymmetrization.lean +++ b/RealRooted/PartialSymmetrization.lean @@ -1,3 +1,4 @@ +import Mathlib.Data.Complex.Basic import RealRooted.Multiaffine /-! From e1e161deb31b439a4baa3efcde54f591db74f8dd Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Mon, 3 Aug 2026 20:26:12 +0000 Subject: [PATCH 45/81] fix: repair degree-box comparator build --- RealRooted/BorceaBranden/FiniteSymbolBasis.lean | 6 +++++- RealRooted/PartialSymmetrization.lean | 2 +- 2 files changed, 6 insertions(+), 2 deletions(-) diff --git a/RealRooted/BorceaBranden/FiniteSymbolBasis.lean b/RealRooted/BorceaBranden/FiniteSymbolBasis.lean index 204d192e3..9df66ea2a 100644 --- a/RealRooted/BorceaBranden/FiniteSymbolBasis.lean +++ b/RealRooted/BorceaBranden/FiniteSymbolBasis.lean @@ -171,7 +171,11 @@ theorem algebraicSymbol_finOne_eq_sum_fin rw [algebraicSymbol] apply Fintype.sum_equiv (degreeOfLEFinOneEquiv n) intro m - simp [finOneDegreeIndex_equiv_apply, boxChoose, + have hindex : finOneDegreeIndex n (m 0) = m := by + apply (degreeOfLEFinOneEquiv n).injective + apply Fin.ext + simp [finOneDegreeIndex, degreeOfLEFinOneEquiv_val, m.2 0] + simp [hindex, boxChoose, rightComplementMonomial, degreeOfLEFinOneEquiv_val] /-- Expand a one-variable algebraic symbol over the natural-number range diff --git a/RealRooted/PartialSymmetrization.lean b/RealRooted/PartialSymmetrization.lean index 111fda0f4..283101de2 100644 --- a/RealRooted/PartialSymmetrization.lean +++ b/RealRooted/PartialSymmetrization.lean @@ -1,4 +1,4 @@ -import Mathlib.Data.Complex.Basic +import Mathlib import RealRooted.Multiaffine /-! From 1ba62e1d11d0e2daae7e277439ff1d4c0449788b Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Mon, 3 Aug 2026 20:31:04 +0000 Subject: [PATCH 46/81] fix: use owning stability and index APIs --- RealRooted/BorceaBranden/FiniteSymbolBasis.lean | 10 ++++++---- RealRooted/PartialSymmetrization.lean | 1 + 2 files changed, 7 insertions(+), 4 deletions(-) diff --git a/RealRooted/BorceaBranden/FiniteSymbolBasis.lean b/RealRooted/BorceaBranden/FiniteSymbolBasis.lean index 9df66ea2a..c4408cf5f 100644 --- a/RealRooted/BorceaBranden/FiniteSymbolBasis.lean +++ b/RealRooted/BorceaBranden/FiniteSymbolBasis.lean @@ -171,10 +171,12 @@ theorem algebraicSymbol_finOne_eq_sum_fin rw [algebraicSymbol] apply Fintype.sum_equiv (degreeOfLEFinOneEquiv n) intro m - have hindex : finOneDegreeIndex n (m 0) = m := by - apply (degreeOfLEFinOneEquiv n).injective - apply Fin.ext - simp [finOneDegreeIndex, degreeOfLEFinOneEquiv_val, m.2 0] + have hindex : finOneDegreeIndex n (m.1 0) = m := by + apply Subtype.ext + apply Finsupp.ext + intro i + rw [Fin.eq_zero i] + simp [finOneDegreeIndex, Nat.min_eq_left (m.2 0)] simp [hindex, boxChoose, rightComplementMonomial, degreeOfLEFinOneEquiv_val] diff --git a/RealRooted/PartialSymmetrization.lean b/RealRooted/PartialSymmetrization.lean index 283101de2..32c090433 100644 --- a/RealRooted/PartialSymmetrization.lean +++ b/RealRooted/PartialSymmetrization.lean @@ -1,5 +1,6 @@ import Mathlib import RealRooted.Multiaffine +import RealRooted.MultivariateStability /-! # Partial symmetrization From 78b55b9314b78dc51dce8852fa58f4d961f8c7b2 Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Mon, 3 Aug 2026 20:31:55 +0000 Subject: [PATCH 47/81] chore: update finite-symbol vars API --- RealRooted/BorceaBranden/FiniteSymbolDegree.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/RealRooted/BorceaBranden/FiniteSymbolDegree.lean b/RealRooted/BorceaBranden/FiniteSymbolDegree.lean index daba03e7e..8de10c4bc 100644 --- a/RealRooted/BorceaBranden/FiniteSymbolDegree.lean +++ b/RealRooted/BorceaBranden/FiniteSymbolDegree.lean @@ -58,7 +58,7 @@ theorem degreeOf_algebraicSymbol_one_inr_le have hmem : Sum.inr i ∈ (rename (Sum.inl : tau → tau ⊕ sigma) (T (basisDegreeOfLE (fun _ : sigma => 1) m))).vars := by - rw [mem_vars] + rw [mem_vars_iff_mem_support] exact ⟨d, hd, Finsupp.mem_support_iff.mpr hdi⟩ obtain ⟨j, _hj, hji⟩ := mem_vars_rename Sum.inl _ hmem exact Sum.inl_ne_inr hji From 3ee82f6378c4138d71f939e91a32e68bacfae15b Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Mon, 3 Aug 2026 20:34:34 +0000 Subject: [PATCH 48/81] feat: define source-block polarization --- .../Applications/DegreeBoxPolarization.lean | 30 +++++++++++++++++-- 1 file changed, 28 insertions(+), 2 deletions(-) diff --git a/RealRooted/BorceaBranden/Applications/DegreeBoxPolarization.lean b/RealRooted/BorceaBranden/Applications/DegreeBoxPolarization.lean index c2915db1b..b0f1d2c1b 100644 --- a/RealRooted/BorceaBranden/Applications/DegreeBoxPolarization.lean +++ b/RealRooted/BorceaBranden/Applications/DegreeBoxPolarization.lean @@ -101,6 +101,30 @@ end RealRooted.BorceaBranden namespace MvPolynomial +/-- The coefficient of source degree `k`, after viewing a polynomial in +`tau ⊕ Fin 1` as a polynomial in the single source variable with coefficients +in the output-variable ring `MvPolynomial tau ℂ`. -/ +noncomputable def sourceCoefficient {τ : Type*} + (P : MvPolynomial (τ ⊕ Fin 1) ℂ) (k : ℕ) : MvPolynomial τ ℂ := + (sumAlgEquiv ℂ (Fin 1) τ + (rename (Equiv.sumComm τ (Fin 1)) P)).coeff + (Finsupp.single default k) + +/-- Polarize only the single source variable of a polynomial whose output +variables are indexed by `τ`. + +This is the one-source-coordinate instance of Borcea--Brändén's operator +`Π↑` from Proposition 2.4 and Lemma 2.5: the source coefficient of degree `k` +is divided by `choose n k`, and the source monomial is replaced by the +elementary symmetric polynomial `e_k` in the `Fin n` source block. -/ +noncomputable def sourceBlockPolarization {τ : Type*} (n : ℕ) + (P : MvPolynomial (τ ⊕ Fin 1) ℂ) : + MvPolynomial (τ ⊕ Fin n) ℂ := + ∑ k ∈ Finset.range (n + 1), + C ((n.choose k : ℂ)⁻¹) * + rename Sum.inl (sourceCoefficient P k) * + rename Sum.inr (esymm (Fin n) ℂ k) + /-- Identify all polarized source variables while leaving output variables unchanged. -/ def sourceDiagonalVariableMap {τ : Type*} {n : ℕ} : @@ -175,8 +199,10 @@ theorem rename_algebraicSymbol_sourcePolarizedOperator_eq_sum sourcePolarizedOperator_basisDegreeOfLE, MvPolynomial.rename_rightComplementMonomial_one m.1 m.2] -/-- Source-side specialization of Borcea--Brändén Lemma 2.5: diagonalizing the -multiaffine source symbol recovers the original degree-box symbol. -/ +/-- Diagonal consequence of the source-side Borcea--Brändén Lemma 2.5 route: +identifying the multiaffine source variables recovers the original degree-box +symbol. The full Lemma 2.5 identity before diagonalization is strictly +stronger and uses `MvPolynomial.sourceBlockPolarization`. -/ theorem rename_algebraicSymbol_sourcePolarizedOperator {τ : Type*} (n : ℕ) (T : degreeOfLE (Fin 1) ℂ (fun _ => n) →ₗ[ℂ] From d4b6344c3fabeeec38e16a6df2525adee7f80f9c Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Mon, 3 Aug 2026 20:40:46 +0000 Subject: [PATCH 49/81] feat: extract source-block coefficients --- .../Applications/DegreeBoxPolarization.lean | 36 +++++++++++++++++++ 1 file changed, 36 insertions(+) diff --git a/RealRooted/BorceaBranden/Applications/DegreeBoxPolarization.lean b/RealRooted/BorceaBranden/Applications/DegreeBoxPolarization.lean index b0f1d2c1b..167a75cc7 100644 --- a/RealRooted/BorceaBranden/Applications/DegreeBoxPolarization.lean +++ b/RealRooted/BorceaBranden/Applications/DegreeBoxPolarization.lean @@ -125,6 +125,42 @@ noncomputable def sourceBlockPolarization {τ : Type*} (n : ℕ) rename Sum.inl (sourceCoefficient P k) * rename Sum.inr (esymm (Fin n) ℂ k) +/-- Extracting a source coefficient commutes with a finite sum. -/ +theorem sourceCoefficient_sum {τ ι : Type*} (s : Finset ι) + (f : ι → MvPolynomial (τ ⊕ Fin 1) ℂ) (k : ℕ) : + sourceCoefficient (∑ i ∈ s, f i) k = + ∑ i ∈ s, sourceCoefficient (f i) k := by + simp [sourceCoefficient, map_sum, coeff_sum] + +/-- Extract the source coefficient of an output polynomial times one source +monomial. -/ +theorem sourceCoefficient_rename_mul_X_pow {τ : Type*} + (q : MvPolynomial τ ℂ) (r k : ℕ) : + sourceCoefficient + (rename (Sum.inl : τ → τ ⊕ Fin 1) q * + X (Sum.inr default) ^ r) k = + if k = r then q else 0 := by + have hpoly : + (sumAlgEquiv ℂ (Fin 1) τ) + (rename (Equiv.sumComm τ (Fin 1)) + (rename (Sum.inl : τ → τ ⊕ Fin 1) q * + X (Sum.inr default) ^ r)) = + C q * X default ^ r := by + simp only [map_mul, map_pow, rename_X, rename_rename, + Equiv.sumComm_apply] + change (sumAlgEquiv ℂ (Fin 1) τ) + (rename (Sum.inr : τ → Fin 1 ⊕ τ) q) * + (sumAlgEquiv ℂ (Fin 1) τ) (X (Sum.inl default)) ^ r = + C q * X default ^ r + rw [show (sumAlgEquiv ℂ (Fin 1) τ) + (rename (Sum.inr : τ → Fin 1 ⊕ τ) q) = C q by + simpa using DFunLike.congr_fun + (sumAlgEquiv_comp_rename_inr ℂ (Fin 1) τ) q] + simp + unfold sourceCoefficient + rw [hpoly, coeff_C_mul, coeff_X_pow] + simp [eq_comm] + /-- Identify all polarized source variables while leaving output variables unchanged. -/ def sourceDiagonalVariableMap {τ : Type*} {n : ℕ} : From 7d83d94e934df8f28b4a8389cc6259d6201ff080 Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Mon, 3 Aug 2026 20:42:04 +0000 Subject: [PATCH 50/81] golf: use canonical degree-box equivalence --- RealRooted/BorceaBranden/FiniteSymbolBasis.lean | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/RealRooted/BorceaBranden/FiniteSymbolBasis.lean b/RealRooted/BorceaBranden/FiniteSymbolBasis.lean index c4408cf5f..b7da23ce4 100644 --- a/RealRooted/BorceaBranden/FiniteSymbolBasis.lean +++ b/RealRooted/BorceaBranden/FiniteSymbolBasis.lean @@ -172,11 +172,10 @@ theorem algebraicSymbol_finOne_eq_sum_fin apply Fintype.sum_equiv (degreeOfLEFinOneEquiv n) intro m have hindex : finOneDegreeIndex n (m.1 0) = m := by - apply Subtype.ext - apply Finsupp.ext - intro i - rw [Fin.eq_zero i] - simp [finOneDegreeIndex, Nat.min_eq_left (m.2 0)] + apply (degreeOfLEFinOneEquiv n).injective + apply Fin.ext + simp [finOneDegreeIndex, degreeOfLEFinOneEquiv_val, + Nat.min_eq_left (m.2 0)] simp [hindex, boxChoose, rightComplementMonomial, degreeOfLEFinOneEquiv_val] From c4a970873fab788c697247afc8acc9639e381fec Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Mon, 3 Aug 2026 20:44:43 +0000 Subject: [PATCH 51/81] feat: isolate normalized source coefficient --- .../Applications/DegreeBoxPolarization.lean | 40 +++++++++++++++++++ 1 file changed, 40 insertions(+) diff --git a/RealRooted/BorceaBranden/Applications/DegreeBoxPolarization.lean b/RealRooted/BorceaBranden/Applications/DegreeBoxPolarization.lean index 167a75cc7..eec76b5fa 100644 --- a/RealRooted/BorceaBranden/Applications/DegreeBoxPolarization.lean +++ b/RealRooted/BorceaBranden/Applications/DegreeBoxPolarization.lean @@ -161,6 +161,46 @@ theorem sourceCoefficient_rename_mul_X_pow {τ : Type*} rw [hpoly, coeff_C_mul, coeff_X_pow] simp [eq_comm] +/-- Extract the source coefficient when the output coefficient has an +additional scalar factor. -/ +theorem sourceCoefficient_C_mul_rename_mul_X_pow {τ : Type*} + (a : ℂ) (q : MvPolynomial τ ℂ) (r k : ℕ) : + sourceCoefficient + (C a * rename (Sum.inl : τ → τ ⊕ Fin 1) q * + X (Sum.inr default) ^ r) k = + if k = r then C a * q else 0 := by + have hterm : + C a * rename (Sum.inl : τ → τ ⊕ Fin 1) q * + X (Sum.inr default) ^ r = + rename Sum.inl (C a * q) * X (Sum.inr default) ^ r := by + simp + rw [hterm, sourceCoefficient_rename_mul_X_pow] + +/-- In a degree-`n` algebraic-symbol-shaped sum, source degree `r` selects the +unique operator term indexed by `n - r`. -/ +theorem sourceCoefficient_symbol_sum {τ : Type*} (n r : ℕ) + (hr : r ≤ n) (q : ℕ → MvPolynomial τ ℂ) : + sourceCoefficient + (∑ k ∈ Finset.range (n + 1), + C (n.choose k : ℂ) * rename Sum.inl (q k) * + X (Sum.inr default) ^ (n - k)) r = + C (n.choose (n - r) : ℂ) * q (n - r) := by + rw [sourceCoefficient_sum] + rw [Finset.sum_eq_single (n - r)] + · rw [sourceCoefficient_C_mul_rename_mul_X_pow] + simp [Nat.sub_sub_self hr] + · intro k hk hne + rw [sourceCoefficient_C_mul_rename_mul_X_pow] + have hk_le : k ≤ n := Nat.le_of_lt_succ (Finset.mem_range.mp hk) + have hnr : r ≠ n - k := by + intro heq + apply hne + lia + rw [if_neg hnr] + · intro hnot + exact (hnot (Finset.mem_range.mpr + (Nat.lt_succ_of_le (Nat.sub_le n r)))).elim + /-- Identify all polarized source variables while leaving output variables unchanged. -/ def sourceDiagonalVariableMap {τ : Type*} {n : ℕ} : From 0651a2b3997c5e53b9413a04da54b17716f15f7d Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Mon, 3 Aug 2026 20:45:46 +0000 Subject: [PATCH 52/81] feat: compute finite-symbol source coefficient --- .../Applications/DegreeBoxPolarization.lean | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) diff --git a/RealRooted/BorceaBranden/Applications/DegreeBoxPolarization.lean b/RealRooted/BorceaBranden/Applications/DegreeBoxPolarization.lean index eec76b5fa..81b692fbd 100644 --- a/RealRooted/BorceaBranden/Applications/DegreeBoxPolarization.lean +++ b/RealRooted/BorceaBranden/Applications/DegreeBoxPolarization.lean @@ -241,6 +241,25 @@ noncomputable section open MvPolynomial +/-- The source-degree coefficient of a one-variable finite algebraic symbol. + +This is the coefficient calculation on the right-hand side of +Borcea--Brändén Lemma 2.5: source degree `r` corresponds to operator degree +`n - r`, with coefficient `choose n (n - r)`. -/ +theorem sourceCoefficient_algebraicSymbol_finOne + {τ : Type*} (n r : ℕ) + (T : degreeOfLE (Fin 1) ℂ (fun _ => n) →ₗ[ℂ] + MvPolynomial τ ℂ) + (hr : r ≤ n) : + sourceCoefficient (algebraicSymbol (fun _ : Fin 1 => n) T) r = + C (n.choose (n - r) : ℂ) * + T (basisDegreeOfLE (R := ℂ) (fun _ : Fin 1 => n) + (finOneDegreeIndex n (n - r))) := by + rw [algebraicSymbol_finOne_eq_sum_range] + exact sourceCoefficient_symbol_sum n r hr fun k => + T (basisDegreeOfLE (R := ℂ) (fun _ : Fin 1 => n) + (finOneDegreeIndex n k)) + lemma finOneDegreeIndex_degree_eq_diagonalDegreeBoxIndex {n : ℕ} (m : {m : Fin n →₀ ℕ // ∀ i, m i ≤ 1}) : finOneDegreeIndex n m.1.degree = diagonalDegreeBoxIndex m := by From 4a48e77432811fc08f6a89f6c7de66b6b1ab3ab0 Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Mon, 3 Aug 2026 20:48:02 +0000 Subject: [PATCH 53/81] Document source polarization definition --- .../BorceaBranden/Applications/DegreeBoxPolarization.lean | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/RealRooted/BorceaBranden/Applications/DegreeBoxPolarization.lean b/RealRooted/BorceaBranden/Applications/DegreeBoxPolarization.lean index 81b692fbd..4b3ef16c7 100644 --- a/RealRooted/BorceaBranden/Applications/DegreeBoxPolarization.lean +++ b/RealRooted/BorceaBranden/Applications/DegreeBoxPolarization.lean @@ -104,6 +104,9 @@ namespace MvPolynomial /-- The coefficient of source degree `k`, after viewing a polynomial in `tau ⊕ Fin 1` as a polynomial in the single source variable with coefficients in the output-variable ring `MvPolynomial tau ℂ`. -/ +/- Source audit: Borcea--Branden, "The Lee--Yang and Polya--Schur Programs. I", +Proposition 2.4, equation (2.2), and Lemma 2.5. This extracts the coefficient +of the source monomial `z^k` while retaining the output-variable polynomial. -/ noncomputable def sourceCoefficient {τ : Type*} (P : MvPolynomial (τ ⊕ Fin 1) ℂ) (k : ℕ) : MvPolynomial τ ℂ := (sumAlgEquiv ℂ (Fin 1) τ @@ -117,6 +120,9 @@ This is the one-source-coordinate instance of Borcea--Brändén's operator `Π↑` from Proposition 2.4 and Lemma 2.5: the source coefficient of degree `k` is divided by `choose n k`, and the source monomial is replaced by the elementary symmetric polynomial `e_k` in the `Fin n` source block. -/ +/- This is exactly the paper's source polarization `Pi^up`: the coefficient of +`z^k` is divided by `choose n k` and `z^k` is replaced by the elementary +symmetric polynomial `e_k` in the new source block. -/ noncomputable def sourceBlockPolarization {τ : Type*} (n : ℕ) (P : MvPolynomial (τ ⊕ Fin 1) ℂ) : MvPolynomial (τ ⊕ Fin n) ℂ := From 0ad2c9d675189448fa8a634fc7a1b926d46ceb5f Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Mon, 3 Aug 2026 20:54:21 +0000 Subject: [PATCH 54/81] Expand lifted algebraic symbol before diagonalization --- .../Applications/DegreeBoxPolarization.lean | 46 +++++++++++++++++++ 1 file changed, 46 insertions(+) diff --git a/RealRooted/BorceaBranden/Applications/DegreeBoxPolarization.lean b/RealRooted/BorceaBranden/Applications/DegreeBoxPolarization.lean index 4b3ef16c7..d77980a7c 100644 --- a/RealRooted/BorceaBranden/Applications/DegreeBoxPolarization.lean +++ b/RealRooted/BorceaBranden/Applications/DegreeBoxPolarization.lean @@ -277,6 +277,52 @@ lemma finOneDegreeIndex_degree_eq_diagonalDegreeBoxIndex /-- Termwise form of the source-polarized algebraic symbol after identifying all polarized source variables. -/ +/-- The multiaffine symbol of the lifted operator before source diagonalization. +This is the left-hand expansion in Borcea--Branden, Lemma 2.5. -/ +theorem algebraicSymbol_sourcePolarizedOperator_eq_sum + {τ : Type*} (n : ℕ) + (T : degreeOfLE (Fin 1) ℂ (fun _ => n) →ₗ[ℂ] + MvPolynomial τ ℂ) : + algebraicSymbol (fun _ : Fin n => 1) + (sourcePolarizedOperator n T) = + ∑ m : {m : Fin n →₀ ℕ // ∀ i, m i ≤ 1}, + rename (Sum.inl : τ → τ ⊕ Fin n) + (T (basisDegreeOfLE (R := ℂ) (fun _ : Fin 1 => n) + (diagonalDegreeBoxIndex m))) * + rightComplementMonomial (R := ℂ) (τ := τ) + (fun _ : Fin n => 1) m.1 := by + rw [algebraicSymbol_eq_sum] + apply Finset.sum_congr rfl + intro m _ + rw [boxChoose_one_of_le_one m.1 m.2, + sourcePolarizedOperator_basisDegreeOfLE] + simp + +/-- Expanding the paper's `Pi^up` on the one-variable symbol cancels the +binomial coefficient and replaces each source monomial by `e_r`. -/ +theorem sourceBlockPolarization_algebraicSymbol_finOne_eq_sum + {τ : Type*} (n : ℕ) + (T : degreeOfLE (Fin 1) ℂ (fun _ => n) →ₗ[ℂ] + MvPolynomial τ ℂ) : + sourceBlockPolarization n + (algebraicSymbol (fun _ : Fin 1 => n) T) = + ∑ r ∈ Finset.range (n + 1), + rename (Sum.inl : τ → τ ⊕ Fin n) + (T (basisDegreeOfLE (R := ℂ) (fun _ : Fin 1 => n) + (finOneDegreeIndex n (n - r)))) * + rename Sum.inr (esymm (Fin n) ℂ r) := by + unfold sourceBlockPolarization + apply Finset.sum_congr rfl + intro r hr + have hr_le : r ≤ n := Nat.le_of_lt_succ (Finset.mem_range.mp hr) + rw [sourceCoefficient_algebraicSymbol_finOne n r T hr_le] + rw [Nat.choose_symm hr_le] + have hchoose : n.choose r ≠ 0 := (Nat.choose_pos hr_le).ne' + rw [map_mul] + simp only [rename_C] + rw [← mul_assoc, ← C_mul] + simp [hchoose] + theorem rename_algebraicSymbol_sourcePolarizedOperator_eq_sum {τ : Type*} (n : ℕ) (T : degreeOfLE (Fin 1) ℂ (fun _ => n) →ₗ[ℂ] From 51f2223cf740607a38f24f2268d1794b77dab71d Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Mon, 3 Aug 2026 21:01:12 +0000 Subject: [PATCH 55/81] Identify multiaffine complementary supports --- .../Applications/DegreeBoxPolarization.lean | 16 ++++++++++++++ .../MvPolynomial/Stability/Symbol.lean | 21 +++++++++++++++++++ 2 files changed, 37 insertions(+) diff --git a/RealRooted/BorceaBranden/Applications/DegreeBoxPolarization.lean b/RealRooted/BorceaBranden/Applications/DegreeBoxPolarization.lean index d77980a7c..5656ca318 100644 --- a/RealRooted/BorceaBranden/Applications/DegreeBoxPolarization.lean +++ b/RealRooted/BorceaBranden/Applications/DegreeBoxPolarization.lean @@ -277,6 +277,22 @@ lemma finOneDegreeIndex_degree_eq_diagonalDegreeBoxIndex /-- Termwise form of the source-polarized algebraic symbol after identifying all polarized source variables. -/ +/-- A degree-one exponent's complementary monomial is indexed by the complement +of the corresponding finite support. -/ +@[simp] +theorem rightComplementMonomial_one_degreeOneExponentEquivFinset_symm + {τ R : Type*} [CommSemiring R] (n : ℕ) (s : Finset (Fin n)) : + rightComplementMonomial (R := R) (τ := τ) (fun _ : Fin n => 1) + ((degreeOneExponentEquivFinset (Fin n)).symm s).1 = + rename (Sum.inr : Fin n → τ ⊕ Fin n) (∏ i ∈ sᶜ, X i) := by + rw [rightComplementMonomial_one_eq_support_compl + ((degreeOneExponentEquivFinset (Fin n)).symm s).1 + ((degreeOneExponentEquivFinset (Fin n)).symm s).2] + have hsupp : + ((degreeOneExponentEquivFinset (Fin n)).symm s).1.support = s := + (degreeOneExponentEquivFinset (Fin n)).apply_symm_apply s + rw [hsupp] + /-- The multiaffine symbol of the lifted operator before source diagonalization. This is the left-hand expansion in Borcea--Branden, Lemma 2.5. -/ theorem algebraicSymbol_sourcePolarizedOperator_eq_sum diff --git a/RealRooted/Mathlib/Algebra/MvPolynomial/Stability/Symbol.lean b/RealRooted/Mathlib/Algebra/MvPolynomial/Stability/Symbol.lean index a8d4441cd..120cb2188 100644 --- a/RealRooted/Mathlib/Algebra/MvPolynomial/Stability/Symbol.lean +++ b/RealRooted/Mathlib/Algebra/MvPolynomial/Stability/Symbol.lean @@ -61,6 +61,27 @@ theorem rightComplementMonomial_eq_prod (κ : σ → ℕ) (m : σ →₀ ℕ) : ∏ i, X (Sum.inr i) ^ (κ i - m i) := by rfl +/-- In a multiaffine box, the complementary monomial is the product over the +complement of the exponent support. -/ +theorem rightComplementMonomial_one_eq_support_compl [DecidableEq σ] + (m : σ →₀ ℕ) (hm : ∀ i, m i ≤ 1) : + rightComplementMonomial (R := R) (τ := τ) (fun _ : σ => 1) m = + rename (Sum.inr : σ → τ ⊕ σ) (∏ i ∈ m.supportᶜ, X i) := by + rw [rightComplementMonomial_eq_prod] + simp only [map_prod, rename_X] + rw [Finset.compl_eq_univ_sdiff, Finset.sdiff_eq_filter, + Finset.prod_filter] + apply Finset.prod_congr rfl + intro i _ + by_cases hi : i ∈ m.support + · have hmi : m i = 1 := by + rcases Nat.le_one_iff_eq_zero_or_eq_one.mp (hm i) with hzero | hone + · exact (Finsupp.mem_support_iff.mp hi hzero).elim + · exact hone + simp [hi, hmi] + · have hmi : m i = 0 := Finsupp.notMem_support_iff.mp hi + simp [hi, hmi] + /-- The finite algebraic symbol of a linear map on a coordinate-wise degree box. Its monomial-basis expansion is `Σ m, choose(κ, m) * T(X^m) * w^(κ-m)`. -/ From ca95ee93c9b3f51f89660779798440ce4d5f56e8 Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Mon, 3 Aug 2026 21:04:29 +0000 Subject: [PATCH 56/81] Repair degree-box polarization infrastructure --- .../Applications/DegreeBoxPolarization.lean | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/RealRooted/BorceaBranden/Applications/DegreeBoxPolarization.lean b/RealRooted/BorceaBranden/Applications/DegreeBoxPolarization.lean index 5656ca318..d94957691 100644 --- a/RealRooted/BorceaBranden/Applications/DegreeBoxPolarization.lean +++ b/RealRooted/BorceaBranden/Applications/DegreeBoxPolarization.lean @@ -30,7 +30,8 @@ theorem sourcePolarizedOperator_comp_polarizationDegreeBoxLinearMap MvPolynomial τ ℂ) : (sourcePolarizedOperator n T).comp (polarizationDegreeBoxLinearMap n) = T := by - ext q + apply LinearMap.ext + intro q change T (diagonalProjectionDegreeBox n (polarizationDegreeBoxLinearMap n q)) = T q rw [diagonalProjectionDegreeBox_comp_polarizationDegreeBoxLinearMap q] @@ -105,7 +106,7 @@ namespace MvPolynomial `tau ⊕ Fin 1` as a polynomial in the single source variable with coefficients in the output-variable ring `MvPolynomial tau ℂ`. -/ /- Source audit: Borcea--Branden, "The Lee--Yang and Polya--Schur Programs. I", -Proposition 2.4, equation (2.2), and Lemma 2.5. This extracts the coefficient +Proposition 2.4, equation (2.2), and Lemma 2.5. This extracts the coefficient of the source monomial `z^k` while retaining the output-variable polynomial. -/ noncomputable def sourceCoefficient {τ : Type*} (P : MvPolynomial (τ ⊕ Fin 1) ℂ) (k : ℕ) : MvPolynomial τ ℂ := @@ -269,11 +270,14 @@ theorem sourceCoefficient_algebraicSymbol_finOne lemma finOneDegreeIndex_degree_eq_diagonalDegreeBoxIndex {n : ℕ} (m : {m : Fin n →₀ ℕ // ∀ i, m i ≤ 1}) : finOneDegreeIndex n m.1.degree = diagonalDegreeBoxIndex m := by + have hm_degree : m.1.degree ≤ n := by + rw [← card_support_eq_degree_of_le_one m.1 m.2] + simpa using Finset.card_le_univ m.1.support apply (degreeOfLEFinOneEquiv n).injective apply Fin.ext simp [finOneDegreeIndex, degreeOfLEFinOneEquiv_val, diagonalDegreeBoxIndex, - Nat.min_eq_left (degree_le_fin_card_of_le_one m.1 m.2)] + Nat.min_eq_left hm_degree] /-- Termwise form of the source-polarized algebraic symbol after identifying all polarized source variables. -/ From 69f33bd2aac6f66284f0f2c93da9162c9bcf1967 Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Mon, 3 Aug 2026 21:07:33 +0000 Subject: [PATCH 57/81] Prove source-polarized symbol identity --- .../Applications/DegreeBoxPolarization.lean | 81 +++++++++++++++++++ 1 file changed, 81 insertions(+) diff --git a/RealRooted/BorceaBranden/Applications/DegreeBoxPolarization.lean b/RealRooted/BorceaBranden/Applications/DegreeBoxPolarization.lean index d94957691..98906710c 100644 --- a/RealRooted/BorceaBranden/Applications/DegreeBoxPolarization.lean +++ b/RealRooted/BorceaBranden/Applications/DegreeBoxPolarization.lean @@ -281,6 +281,33 @@ lemma finOneDegreeIndex_degree_eq_diagonalDegreeBoxIndex /-- Termwise form of the source-polarized algebraic symbol after identifying all polarized source variables. -/ +/-- Summation over finite subsets is invariant under taking complements. -/ +theorem sum_finset_compl + {M α : Type*} [AddCommMonoid M] [Fintype α] [DecidableEq α] + (f : Finset α → M) : + ∑ s : Finset α, f sᶜ = ∑ s, f s := by + let e : Finset α ≃ Finset α := + { toFun := fun s => sᶜ + invFun := fun s => sᶜ + left_inv := compl_compl + right_inv := compl_compl } + exact e.sum_comp f + +/-- Complement reindexing exchanges a support cardinality with its codimension. -/ +theorem sum_finset_card_compl + {M : Type*} [AddCommMonoid M] (n : ℕ) + (f : ℕ → Finset (Fin n) → M) : + ∑ s : Finset (Fin n), f s.card sᶜ = + ∑ s, f (n - s.card) s := by + rw [← sum_finset_compl (fun s : Finset (Fin n) => + f (n - s.card) s)] + apply Finset.sum_congr rfl + intro s _ + rw [Finset.card_compl] + simp only [Fintype.card_fin] + have hs : s.card ≤ n := by simpa using Finset.card_le_univ s + rw [Nat.sub_sub_self hs] + /-- A degree-one exponent's complementary monomial is indexed by the complement of the corresponding finite support. -/ @[simp] @@ -297,6 +324,43 @@ theorem rightComplementMonomial_one_degreeOneExponentEquivFinset_symm (degreeOneExponentEquivFinset (Fin n)).apply_symm_apply s rw [hsupp] +/-- Grouping squarefree monomials by support cardinality gives `esymm`. -/ +theorem sum_finset_card_prod_eq_sum_esymm + {τ : Type*} (n : ℕ) (q : ℕ → MvPolynomial τ ℂ) : + (∑ s : Finset (Fin n), + rename (Sum.inl : τ → τ ⊕ Fin n) (q (n - s.card)) * + rename Sum.inr (∏ i ∈ s, X i)) = + ∑ r ∈ Finset.range (n + 1), + rename (Sum.inl : τ → τ ⊕ Fin n) (q (n - r)) * + rename Sum.inr (esymm (Fin n) ℂ r) := by + rw [sum_finset_eq_sum_powersetCard] + apply Finset.sum_congr rfl + intro r _ + rw [esymm, map_sum, Finset.mul_sum] + simp only [map_prod, rename_X] + apply Finset.sum_congr rfl + intro s hs + rw [(Finset.mem_powersetCard.mp hs).2] + +/-- Complementing zero-one exponent supports and grouping by cardinality gives +the elementary-symmetric expansion used in Borcea--Branden, Lemma 2.5. -/ +theorem sum_degreeOneExponent_rightComplementMonomial_eq_sum_esymm + {τ : Type*} (n : ℕ) (q : ℕ → MvPolynomial τ ℂ) : + (∑ m : {m : Fin n →₀ ℕ // ∀ i, m i ≤ 1}, + rename (Sum.inl : τ → τ ⊕ Fin n) (q m.1.degree) * + rightComplementMonomial (R := ℂ) (τ := τ) + (fun _ : Fin n => 1) m.1) = + ∑ r ∈ Finset.range (n + 1), + rename (Sum.inl : τ → τ ⊕ Fin n) (q (n - r)) * + rename Sum.inr (esymm (Fin n) ℂ r) := by + rw [sum_degreeOneExponent_eq_sum_finset] + simp only [degree_degreeOneExponentEquivFinset_symm, + rightComplementMonomial_one_degreeOneExponentEquivFinset_symm] + rw [sum_finset_card_compl n (fun k s => + rename (Sum.inl : τ → τ ⊕ Fin n) (q k) * + rename Sum.inr (∏ i ∈ s, X i))] + exact sum_finset_card_prod_eq_sum_esymm n q + /-- The multiaffine symbol of the lifted operator before source diagonalization. This is the left-hand expansion in Borcea--Branden, Lemma 2.5. -/ theorem algebraicSymbol_sourcePolarizedOperator_eq_sum @@ -343,6 +407,23 @@ theorem sourceBlockPolarization_algebraicSymbol_finOne_eq_sum rw [← mul_assoc, ← C_mul] simp [hchoose] +/-- Borcea--Branden, Lemma 2.5: source polarization of an operator polarizes +its finite algebraic symbol in the source-variable block. -/ +theorem algebraicSymbol_sourcePolarizedOperator + {τ : Type*} (n : ℕ) + (T : degreeOfLE (Fin 1) ℂ (fun _ => n) →ₗ[ℂ] + MvPolynomial τ ℂ) : + algebraicSymbol (fun _ : Fin n => 1) + (sourcePolarizedOperator n T) = + sourceBlockPolarization n + (algebraicSymbol (fun _ : Fin 1 => n) T) := by + rw [algebraicSymbol_sourcePolarizedOperator_eq_sum, + sourceBlockPolarization_algebraicSymbol_finOne_eq_sum] + simpa only [← finOneDegreeIndex_degree_eq_diagonalDegreeBoxIndex] using + sum_degreeOneExponent_rightComplementMonomial_eq_sum_esymm n + (fun k => T (basisDegreeOfLE (R := ℂ) (fun _ : Fin 1 => n) + (finOneDegreeIndex n k))) + theorem rename_algebraicSymbol_sourcePolarizedOperator_eq_sum {τ : Type*} (n : ℕ) (T : degreeOfLE (Fin 1) ℂ (fun _ => n) →ₗ[ℂ] From bb092a5be03a2a5da78bb3eccacd39901b830723 Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Mon, 3 Aug 2026 21:18:20 +0000 Subject: [PATCH 58/81] Clean up degree-box proof scaffolding --- .../Applications/DegreeBoxPolarization.lean | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/RealRooted/BorceaBranden/Applications/DegreeBoxPolarization.lean b/RealRooted/BorceaBranden/Applications/DegreeBoxPolarization.lean index 98906710c..9b59f9b25 100644 --- a/RealRooted/BorceaBranden/Applications/DegreeBoxPolarization.lean +++ b/RealRooted/BorceaBranden/Applications/DegreeBoxPolarization.lean @@ -279,10 +279,8 @@ lemma finOneDegreeIndex_degree_eq_diagonalDegreeBoxIndex diagonalDegreeBoxIndex, Nat.min_eq_left hm_degree] -/-- Termwise form of the source-polarized algebraic symbol after identifying -all polarized source variables. -/ /-- Summation over finite subsets is invariant under taking complements. -/ -theorem sum_finset_compl +private theorem sum_finset_compl {M α : Type*} [AddCommMonoid M] [Fintype α] [DecidableEq α] (f : Finset α → M) : ∑ s : Finset α, f sᶜ = ∑ s, f s := by @@ -294,7 +292,7 @@ theorem sum_finset_compl exact e.sum_comp f /-- Complement reindexing exchanges a support cardinality with its codimension. -/ -theorem sum_finset_card_compl +private theorem sum_finset_card_compl {M : Type*} [AddCommMonoid M] (n : ℕ) (f : ℕ → Finset (Fin n) → M) : ∑ s : Finset (Fin n), f s.card sᶜ = @@ -311,7 +309,7 @@ theorem sum_finset_card_compl /-- A degree-one exponent's complementary monomial is indexed by the complement of the corresponding finite support. -/ @[simp] -theorem rightComplementMonomial_one_degreeOneExponentEquivFinset_symm +private theorem rightComplementMonomial_one_degreeOneExponentEquivFinset_symm {τ R : Type*} [CommSemiring R] (n : ℕ) (s : Finset (Fin n)) : rightComplementMonomial (R := R) (τ := τ) (fun _ : Fin n => 1) ((degreeOneExponentEquivFinset (Fin n)).symm s).1 = @@ -325,7 +323,7 @@ theorem rightComplementMonomial_one_degreeOneExponentEquivFinset_symm rw [hsupp] /-- Grouping squarefree monomials by support cardinality gives `esymm`. -/ -theorem sum_finset_card_prod_eq_sum_esymm +private theorem sum_finset_card_prod_eq_sum_esymm {τ : Type*} (n : ℕ) (q : ℕ → MvPolynomial τ ℂ) : (∑ s : Finset (Fin n), rename (Sum.inl : τ → τ ⊕ Fin n) (q (n - s.card)) * @@ -344,7 +342,7 @@ theorem sum_finset_card_prod_eq_sum_esymm /-- Complementing zero-one exponent supports and grouping by cardinality gives the elementary-symmetric expansion used in Borcea--Branden, Lemma 2.5. -/ -theorem sum_degreeOneExponent_rightComplementMonomial_eq_sum_esymm +private theorem sum_degreeOneExponent_rightComplementMonomial_eq_sum_esymm {τ : Type*} (n : ℕ) (q : ℕ → MvPolynomial τ ℂ) : (∑ m : {m : Fin n →₀ ℕ // ∀ i, m i ≤ 1}, rename (Sum.inl : τ → τ ⊕ Fin n) (q m.1.degree) * @@ -424,6 +422,8 @@ theorem algebraicSymbol_sourcePolarizedOperator (fun k => T (basisDegreeOfLE (R := ℂ) (fun _ : Fin 1 => n) (finOneDegreeIndex n k))) +/-- Termwise form of the source-polarized algebraic symbol after identifying +all polarized source variables. -/ theorem rename_algebraicSymbol_sourcePolarizedOperator_eq_sum {τ : Type*} (n : ℕ) (T : degreeOfLE (Fin 1) ℂ (fun _ => n) →ₗ[ℂ] From 8fc0d73217df9b85159c9d769f0b55ec17ac2f11 Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Mon, 3 Aug 2026 21:23:33 +0000 Subject: [PATCH 59/81] Bound polar derivative degree --- RealRooted/Apolarity.lean | 37 +++++++++++++++++++++++++++++++++++++ 1 file changed, 37 insertions(+) diff --git a/RealRooted/Apolarity.lean b/RealRooted/Apolarity.lean index 0de1aea82..46dc2a322 100644 --- a/RealRooted/Apolarity.lean +++ b/RealRooted/Apolarity.lean @@ -589,6 +589,43 @@ theorem grace_apolarity_closedBall {n : Nat} {c : ℂ} {r : ℝ} {f g : ℂ[X]} def polarDeriv (n : Nat) (ζ : ℂ) (A : ℂ[X]) : ℂ[X] := C (n : ℂ) * A + (C ζ - X) * derivative A +/-- The polar derivative lowers the ambient degree bound by one. This is the +bounded-degree invariant needed in the Grace apolarity induction. -/ +theorem polarDeriv_natDegree_le + {n : Nat} {ζ : ℂ} {A : ℂ[X]} + (hn : 1 ≤ n) (hA : A.natDegree ≤ n) : + (polarDeriv n ζ A).natDegree ≤ n - 1 := by + rw [Polynomial.natDegree_le_iff_degree_le, + Polynomial.degree_le_iff_coeff_zero] + intro m hm + have hm' : n - 1 < m := by exact_mod_cast hm + have hnm : n ≤ m := by lia + rcases hnm.eq_or_lt with rfl | hlt + · have hnext : A.coeff (n + 1) = 0 := + Polynomial.coeff_eq_zero_of_natDegree_lt + (lt_of_le_of_lt hA (Nat.lt_succ_self n)) + unfold polarDeriv + rw [sub_mul] + simp only [Polynomial.coeff_add, Polynomial.coeff_sub, + Polynomial.coeff_C_mul, Polynomial.coeff_derivative, hnext] + rw [show n = (n - 1) + 1 by lia, Polynomial.coeff_X_mul, + Polynomial.coeff_derivative] + norm_num + ring + · have hm0 : A.coeff m = 0 := + Polynomial.coeff_eq_zero_of_natDegree_lt (lt_of_le_of_lt hA hlt) + have hm1 : A.coeff (m + 1) = 0 := + Polynomial.coeff_eq_zero_of_natDegree_lt + (lt_of_le_of_lt hA (hlt.trans (Nat.lt_succ_self m))) + unfold polarDeriv + rw [sub_mul] + simp only [Polynomial.coeff_add, Polynomial.coeff_sub, + Polynomial.coeff_C_mul, Polynomial.coeff_derivative, hm0, hm1] + rw [show m = (m - 1) + 1 by lia, Polynomial.coeff_X_mul, + Polynomial.coeff_derivative] + rw [show m - 1 + 1 = m by lia, hm0] + simp + /-- The coefficient shift dual to the polar derivative: `(polarShift ζ f).coeff k = f.coeff k + ζ * f.coeff (k + 1)`. -/ def polarShift (ζ : ℂ) (f : ℂ[X]) : ℂ[X] := f + C ζ * divX f From c958eb8e89d8af67844ef36c2970d4e221ca12cc Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Mon, 3 Aug 2026 21:29:31 +0000 Subject: [PATCH 60/81] Generalize polar derivative root containment --- RealRooted/GraceHalfPlane.lean | 99 ++++++++++++++++++++++++++++++++++ 1 file changed, 99 insertions(+) diff --git a/RealRooted/GraceHalfPlane.lean b/RealRooted/GraceHalfPlane.lean index e5a1b6916..20eca8c4b 100644 --- a/RealRooted/GraceHalfPlane.lean +++ b/RealRooted/GraceHalfPlane.lean @@ -84,6 +84,105 @@ theorem mem_lowerHalf_of_recip_avg {b : ℝ} {w ζ : ℂ} simp_all grind +/-- The reciprocal-average conclusion remains valid when the numerator is an +ambient cardinality at least as large as the multiset cardinality. This is the +half-plane form of adjoining roots at infinity in Grace's theorem. -/ +theorem mem_lowerHalf_of_recip_sum_of_card_le + {b : ℝ} {w ζ : ℂ} {n : ℕ} + (S : Multiset ℂ) (hS : S ≠ 0) (hcard : S.card ≤ n) + (hw : w ∉ lowerHalf b) + (hz : ∀ z ∈ S, z ∈ lowerHalf b) + (hζ : (n : ℂ) / (w - ζ) = + (S.map (fun z ↦ 1 / (w - z))).sum) : + ζ ∈ lowerHalf b := by + let d : ℕ := S.card + have hd : 0 < d := by + simpa [d] using Multiset.card_pos.mpr hS + have hn : 0 < n := lt_of_lt_of_le hd (by simpa [d] using hcard) + let t : ℝ := (d : ℝ) / (n : ℝ) + have ht_pos : 0 < t := by + dsimp [t] + positivity + have ht_le : t ≤ 1 := by + dsimp [t] + rw [div_le_one] + · exact_mod_cast hcard + · exact_mod_cast hn + let ζ' : ℂ := w - (t : ℂ) * (w - ζ) + have hscaled : + (S.card : ℂ) / (w - ζ') = + (S.map (fun z ↦ 1 / (w - z))).sum := by + rw [← hζ] + dsimp [ζ', t, d] + have hn0 : (n : ℂ) ≠ 0 := by exact_mod_cast hn.ne' + have hd0 : (S.card : ℂ) ≠ 0 := by + exact_mod_cast (Multiset.card_pos.mpr hS).ne' + by_cases hwζ : w - ζ = 0 + · simp [hwζ] + · push_cast + field_simp [hn0, hd0, hwζ] + ring + have hζ' : ζ' ∈ lowerHalf b := + mem_lowerHalf_of_recip_avg S hS hw hz hscaled + have hw_im : b < w.im := by + simpa [lowerHalf] using hw + simp only [mem_lowerHalf] at hζ' ⊢ + dsimp [ζ'] at hζ' + simp only [Complex.sub_im, Complex.mul_im, + Complex.ofReal_re, Complex.ofReal_im, zero_mul, add_zero] at hζ' + nlinarith + +/-- A polar derivative preserves a closed lower half-plane when its ambient +degree only bounds, rather than equals, the polynomial degree. -/ +theorem polarDeriv_rootsIn_lowerHalf_of_natDegree_le + {n : Nat} {b : ℝ} {ζ : ℂ} {A : ℂ[X]} + (hn : 1 ≤ n) (hA : A.natDegree ≤ n) + (hAroots : A.RootsIn (lowerHalf b)) + (hζ : ζ ∉ lowerHalf b) : + (polarDeriv n ζ A).RootsIn (lowerHalf b) := by + intro w hw0 + have hn0 : (n : ℂ) ≠ 0 := by + exact_mod_cast (show n ≠ 0 by lia) + by_cases hA0 : A.natDegree = 0 + · have hder : derivative A = 0 := + Polynomial.derivative_eq_zero.mpr hA0 + apply hAroots w + have h : (n : ℂ) * eval w A = 0 := by + simpa only [IsRoot, polarDeriv, hder, mul_zero, add_zero, + eval_mul, eval_C] using hw0 + exact (mul_eq_zero.mp h).resolve_left hn0 + · by_contra hwmem + have hAw : eval w A ≠ 0 := + fun h ↦ hwmem (hAroots w h) + have heq : (n : ℂ) * eval w A + + (ζ - w) * eval w (derivative A) = 0 := by + have h := hw0 + simp only [IsRoot, polarDeriv, eval_add, eval_mul, + eval_sub, eval_C, eval_X] at h + simp_all + have hwζ : w - ζ ≠ 0 := by grind + have hsplit : A.Splits := IsAlgClosed.splits A + have hcard : A.roots.card = A.natDegree := + splits_iff_card_roots.mp hsplit + have hroots_ne : A.roots ≠ 0 := by + rw [← Multiset.card_pos, hcard] + exact Nat.pos_of_ne_zero hA0 + have hcard_le : A.roots.card ≤ n := hcard.trans_le hA + have hlog : eval w (derivative A) / eval w A = + (A.roots.map (fun z ↦ 1 / (w - z))).sum := + hsplit.eval_derivative_div_eval_of_ne_zero hAw + have hratio : eval w (derivative A) / eval w A = + (n : ℂ) / (w - ζ) := by + grind + have hscaled : (n : ℂ) / (w - ζ) = + (A.roots.map (fun z ↦ 1 / (w - z))).sum := + hratio.symm.trans hlog + have : ζ ∈ lowerHalf b := by + exact mem_lowerHalf_of_recip_sum_of_card_le + A.roots hroots_ne hcard_le hwmem + (fun z hz ↦ hAroots z (isRoot_of_mem_roots hz)) hscaled + exact hζ this + theorem multiset_avg_mem_lowerHalf {b : ℝ} (S : Multiset ℂ) (hS : S ≠ 0) (hz : ∀ z ∈ S, z ∈ lowerHalf b) : S.sum / (S.card : ℂ) ∈ lowerHalf b := by From a843543f088b98904687b0be35e423ce84cf2075 Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Mon, 3 Aug 2026 21:33:16 +0000 Subject: [PATCH 61/81] Generalize Grace lower-half degree bound --- RealRooted/GraceHalfPlane.lean | 19 +++++++++---------- RealRooted/Hadamard.lean | 2 +- RealRooted/Polarization.lean | 2 +- 3 files changed, 11 insertions(+), 12 deletions(-) diff --git a/RealRooted/GraceHalfPlane.lean b/RealRooted/GraceHalfPlane.lean index 20eca8c4b..d6d03c86f 100644 --- a/RealRooted/GraceHalfPlane.lean +++ b/RealRooted/GraceHalfPlane.lean @@ -298,7 +298,7 @@ theorem polarDeriv_natDegree_lowerHalf {n : Nat} {b : ℝ} {ζ : ℂ} private theorem grace_aux_lowerHalf {b : ℝ} : ∀ (n : Nat) (f g : ℂ[X]), - (binomialLift n f).natDegree = n → (binomialLift n g).natDegree = n → + (binomialLift n f).natDegree ≤ n → (binomialLift n g).natDegree = n → AreApolar n f g → (binomialLift n f).RootsIn (lowerHalf b) → (binomialLift n g).HasRootIn (lowerHalf b) := by intro n @@ -324,18 +324,17 @@ private theorem grace_aux_lowerHalf {b : ℝ} : by_cases hζ' : ζ ∈ lowerHalf b · exact ⟨ζ, hζ, hζ'⟩ · set f' := polarShift ζ f - have hf' : (binomialLift (n - 1) f').natDegree = n - 1 := by - have hf' : (polarDeriv n ζ (binomialLift n f)).natDegree = n - 1 := by - apply polarDeriv_natDegree_lowerHalf + have hf' : (binomialLift (n - 1) f').natDegree ≤ n - 1 := by + have hf' : (polarDeriv n ζ (binomialLift n f)).natDegree ≤ n - 1 := by + apply polarDeriv_natDegree_le · grind - · simp [*] - · exact hroots - · simp [*] + · exact hf rw [polarDeriv_binomialLift (Nat.pos_of_ne_zero hn) ζ f] at hf' rwa [Polynomial.natDegree_C_mul] at hf' simp_all have hf'_roots : (binomialLift (n - 1) f').RootsIn (lowerHalf b) := by - have := polarDeriv_rootsIn_lowerHalf (Nat.pos_of_ne_zero hn) hf hroots hζ' + have := polarDeriv_rootsIn_lowerHalf_of_natDegree_le + (Nat.pos_of_ne_zero hn) hf hroots hζ' have := polarDeriv_binomialLift (Nat.pos_of_ne_zero hn) ζ f simp_all [RootsIn] grind @@ -363,7 +362,7 @@ private theorem grace_aux_lowerHalf {b : ℝ} : exact ⟨w, by replace hg' := congr_arg (Polynomial.eval w) hg'; simp_all⟩ theorem grace_apolarity_lowerHalf {n : Nat} {b : ℝ} {f g : ℂ[X]} - (hf : (binomialLift n f).natDegree = n) (hg : (binomialLift n g).natDegree = n) + (hf : (binomialLift n f).natDegree ≤ n) (hg : (binomialLift n g).natDegree = n) (hap : AreApolar n f g) (hroots : (binomialLift n f).RootsIn (lowerHalf b)) : (binomialLift n g).HasRootIn (lowerHalf b) := @@ -440,7 +439,7 @@ theorem grace_apolarity_upperHalf {n : Nat} {b : ℝ} {f g : ℂ[X]} simp only [mem_lowerHalf] linarith obtain ⟨w, hwroot, hwmem⟩ := - grace_apolarity_lowerHalf hfhat hghat haphat hroothat + grace_apolarity_lowerHalf hfhat.le hghat haphat hroothat refine ⟨-w, ?_, ?_⟩ · rw [negComp_binomialLift] at hwroot simp only [Polynomial.IsRoot, negComp, Polynomial.eval_comp, Polynomial.eval_neg, diff --git a/RealRooted/Hadamard.lean b/RealRooted/Hadamard.lean index 84e615737..bee0e3b4b 100644 --- a/RealRooted/Hadamard.lean +++ b/RealRooted/Hadamard.lean @@ -1933,7 +1933,7 @@ theorem exists_apolarTwist_root_of_grace_lowerHalf {n : Nat} {b : ℝ} (binomialLift n (apolarTwist n z g)).HasRootIn (lowerHalf b) := by have hap : AreApolar n f (apolarTwist n z g) := (areApolar_apolarTwist_iff n f g z).2 hcomp - exact grace_apolarity_lowerHalf hf htw hap hroots + exact grace_apolarity_lowerHalf hf.le htw hap hroots theorem exists_apolarTwist_root_of_grace_upperHalf {n : Nat} {b : ℝ} {f g : ℂ[X]} {z : ℂ} diff --git a/RealRooted/Polarization.lean b/RealRooted/Polarization.lean index f11ab88d5..e0269c5ec 100644 --- a/RealRooted/Polarization.lean +++ b/RealRooted/Polarization.lean @@ -410,7 +410,7 @@ theorem mvUpperHalfPlaneStable_reducedPolarization {n : ℕ} {f : ℂ[X]} intro w hw exact not_lt.mp (fun hwpos => hstable w hwpos hw) obtain ⟨w, hwroot, hwlower⟩ := - grace_apolarity_lowerHalf hdeg hgdeg hap hroots + grace_apolarity_lowerHalf hdeg.le hgdeg hap hroots obtain ⟨i, hwi⟩ := exists_eq_of_isRoot_polarizationRootPolynomial (hg ▸ hwroot) rw [hwi] at hwlower From 236764349a5442a29d841dc912fe3665c55f2d18 Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Mon, 3 Aug 2026 21:35:36 +0000 Subject: [PATCH 62/81] Golf bounded Grace proof plumbing --- RealRooted/GraceHalfPlane.lean | 21 +++++++-------------- 1 file changed, 7 insertions(+), 14 deletions(-) diff --git a/RealRooted/GraceHalfPlane.lean b/RealRooted/GraceHalfPlane.lean index d6d03c86f..314ca21b6 100644 --- a/RealRooted/GraceHalfPlane.lean +++ b/RealRooted/GraceHalfPlane.lean @@ -95,11 +95,9 @@ theorem mem_lowerHalf_of_recip_sum_of_card_le (hζ : (n : ℂ) / (w - ζ) = (S.map (fun z ↦ 1 / (w - z))).sum) : ζ ∈ lowerHalf b := by - let d : ℕ := S.card - have hd : 0 < d := by - simpa [d] using Multiset.card_pos.mpr hS - have hn : 0 < n := lt_of_lt_of_le hd (by simpa [d] using hcard) - let t : ℝ := (d : ℝ) / (n : ℝ) + have hd : 0 < S.card := Multiset.card_pos.mpr hS + have hn : 0 < n := lt_of_lt_of_le hd hcard + let t : ℝ := (S.card : ℝ) / (n : ℝ) have ht_pos : 0 < t := by dsimp [t] positivity @@ -113,7 +111,7 @@ theorem mem_lowerHalf_of_recip_sum_of_card_le (S.card : ℂ) / (w - ζ') = (S.map (fun z ↦ 1 / (w - z))).sum := by rw [← hζ] - dsimp [ζ', t, d] + dsimp [ζ', t] have hn0 : (n : ℂ) ≠ 0 := by exact_mod_cast hn.ne' have hd0 : (S.card : ℂ) ≠ 0 := by exact_mod_cast (Multiset.card_pos.mpr hS).ne' @@ -168,15 +166,10 @@ theorem polarDeriv_rootsIn_lowerHalf_of_natDegree_le rw [← Multiset.card_pos, hcard] exact Nat.pos_of_ne_zero hA0 have hcard_le : A.roots.card ≤ n := hcard.trans_le hA - have hlog : eval w (derivative A) / eval w A = - (A.roots.map (fun z ↦ 1 / (w - z))).sum := - hsplit.eval_derivative_div_eval_of_ne_zero hAw - have hratio : eval w (derivative A) / eval w A = - (n : ℂ) / (w - ζ) := by - grind have hscaled : (n : ℂ) / (w - ζ) = - (A.roots.map (fun z ↦ 1 / (w - z))).sum := - hratio.symm.trans hlog + (A.roots.map (fun z ↦ 1 / (w - z))).sum := by + rw [← hsplit.eval_derivative_div_eval_of_ne_zero hAw] + grind have : ζ ∈ lowerHalf b := by exact mem_lowerHalf_of_recip_sum_of_card_le A.roots hroots_ne hcard_le hwmem From ff4c8242d6e1f731865ae4a7fdfbe81f8715381f Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Mon, 3 Aug 2026 21:38:52 +0000 Subject: [PATCH 63/81] Generalize polarization stability to bounded degree --- RealRooted/Polarization.lean | 14 +++++++++----- RealRooted/RectangularPolarization.lean | 6 +++--- 2 files changed, 12 insertions(+), 8 deletions(-) diff --git a/RealRooted/Polarization.lean b/RealRooted/Polarization.lean index e0269c5ec..0cfc1f089 100644 --- a/RealRooted/Polarization.lean +++ b/RealRooted/Polarization.lean @@ -393,8 +393,12 @@ theorem eval_reducedPolarization_eq_apolarPairing_of_binomialLift_eq_rootPolynom /-- Grace--Walsh--Szego for reduced coefficients: exact-degree upper-half-plane stability is preserved by polarization. -/ +/- Borcea--Branden, arXiv:0809.0401, Proposition 2.4. The source polynomial +has degree at most `n`; exact degree is unnecessary because the upper half-plane +is a convex circular domain in the Grace--Walsh--Szego theorem. The auxiliary +root polynomial used below still has exact degree `n`. -/ theorem mvUpperHalfPlaneStable_reducedPolarization {n : ℕ} {f : ℂ[X]} - (hdeg : (binomialLift n f).natDegree = n) + (hdeg : (binomialLift n f).natDegree ≤ n) (hstable : ∀ w : ℂ, 0 < w.im → (binomialLift n f).eval w ≠ 0) : MvUpperHalfPlaneStable (reducedPolarization n f) := by intro z hz hzero @@ -410,7 +414,7 @@ theorem mvUpperHalfPlaneStable_reducedPolarization {n : ℕ} {f : ℂ[X]} intro w hw exact not_lt.mp (fun hwpos => hstable w hwpos hw) obtain ⟨w, hwroot, hwlower⟩ := - grace_apolarity_lowerHalf hdeg.le hgdeg hap hroots + grace_apolarity_lowerHalf hdeg hgdeg hap hroots obtain ⟨i, hwi⟩ := exists_eq_of_isRoot_polarizationRootPolynomial (hg ▸ hwroot) rw [hwi] at hwlower @@ -419,13 +423,13 @@ theorem mvUpperHalfPlaneStable_reducedPolarization {n : ℕ} {f : ℂ[X]} /-- Exact-degree upper-half-plane stability is preserved by univariate polarization. -/ theorem mvUpperHalfPlaneStable_polarization {n : ℕ} {p : ℂ[X]} - (hdeg : p.natDegree = n) + (hdeg : p.natDegree ≤ n) (hstable : ∀ w : ℂ, 0 < w.im → p.eval w ≠ 0) : MvUpperHalfPlaneStable (polarization n p) := by unfold polarization apply mvUpperHalfPlaneStable_reducedPolarization - · rw [binomialLift_binomialUnlift hdeg.le, hdeg] - · simpa [binomialLift_binomialUnlift hdeg.le] using hstable + · simpa only [binomialLift_binomialUnlift hdeg] using hdeg + · simpa only [binomialLift_binomialUnlift hdeg] using hstable end diff --git a/RealRooted/RectangularPolarization.lean b/RealRooted/RectangularPolarization.lean index 27c9e7649..18fd92efa 100644 --- a/RealRooted/RectangularPolarization.lean +++ b/RealRooted/RectangularPolarization.lean @@ -262,7 +262,7 @@ theorem upperHalfPlaneStable_rectangularLeftSlice exact mvUpperHalfPlaneStable_polarization (natDegree_rectangularRightSlice_eq hpdeg hplead (fun hzero => by rw [hzero] at hx - simp at hx)) + simp at hx)).le (upperHalfPlaneStable_rectangularRightSlice hpdeg.le hstable hx) y hy /-- Rectangular polarization preserves upper-half-plane stability. This is the @@ -279,8 +279,8 @@ theorem mvUpperHalfPlaneStable_rectangularPolarization cases i <;> rfl rw [hz_elim, eval_rectangularPolarization_eq_eval_polarization_leftSlice] apply mvUpperHalfPlaneStable_polarization - · exact natDegree_rectangularLeftSlice_eq hpdeg hplead - (fun i => hz (Sum.inr i)) + · exact (natDegree_rectangularLeftSlice_eq hpdeg hplead + (fun i => hz (Sum.inr i))).le · exact upperHalfPlaneStable_rectangularLeftSlice hpdeg hplead hstable (fun i => hz (Sum.inr i)) · exact fun i => hz (Sum.inl i) From 6607b5b2cecf1eb63e22b91425bb1a18695c2d85 Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Mon, 3 Aug 2026 21:50:34 +0000 Subject: [PATCH 64/81] Commute source polarization with specialization --- .../Applications/DegreeBoxPolarization.lean | 101 ++++++++++++++++++ 1 file changed, 101 insertions(+) diff --git a/RealRooted/BorceaBranden/Applications/DegreeBoxPolarization.lean b/RealRooted/BorceaBranden/Applications/DegreeBoxPolarization.lean index 9b59f9b25..ea821dc58 100644 --- a/RealRooted/BorceaBranden/Applications/DegreeBoxPolarization.lean +++ b/RealRooted/BorceaBranden/Applications/DegreeBoxPolarization.lean @@ -132,6 +132,107 @@ noncomputable def sourceBlockPolarization {τ : Type*} (n : ℕ) rename Sum.inl (sourceCoefficient P k) * rename Sum.inr (esymm (Fin n) ℂ k) +private theorem + coeff_uniqueAlgEquiv_specializeLeft_eq_eval_sourceCoefficient + {τ : Type*} (P : MvPolynomial (τ ⊕ Fin 1) ℂ) + (x : τ → ℂ) (k : ℕ) : + ((MvPolynomial.uniqueAlgEquiv ℂ (Fin 1)) + (_root_.RealRooted.specializeLeft x P)).coeff k = + MvPolynomial.eval x (sourceCoefficient P k) := by + have hspecial : + _root_.RealRooted.specializeLeft x P = + MvPolynomial.map (MvPolynomial.eval x) + (sumAlgEquiv ℂ (Fin 1) τ + (rename (Equiv.sumComm τ (Fin 1)) P)) := by + unfold _root_.RealRooted.specializeLeft + change + (MvPolynomial.aeval + (Sum.elim (MvPolynomial.C ∘ x) MvPolynomial.X)) P = + ((MvPolynomial.mapAlgHom (MvPolynomial.aeval x)).comp + ((sumAlgEquiv ℂ (Fin 1) τ).toAlgHom.comp + (rename (Equiv.sumComm τ (Fin 1))))) P + congr 1 + apply MvPolynomial.algHom_ext + rintro (i | i) <;> + simp [Function.comp_def, Equiv.sumComm_apply] + rw [MvPolynomial.coeff_uniqueAlgEquiv, hspecial, + MvPolynomial.coeff_map] + change + MvPolynomial.eval x + ((sumAlgEquiv ℂ (Fin 1) τ + (rename (Equiv.sumComm τ (Fin 1)) P)).coeff + (Finsupp.single default k)) = + MvPolynomial.eval x (sourceCoefficient P k) + rfl + +/- Borcea--Branden, arXiv:0809.0401, Proposition 2.4 and equation (2.2). +Specializing the output block commutes with source polarization. The ambient +degree cap remains `n`, even when specialization lowers the source degree. -/ +theorem specializeLeft_sourceBlockPolarization + {τ : Type*} (n : ℕ) (P : MvPolynomial (τ ⊕ Fin 1) ℂ) + (x : τ → ℂ) : + _root_.RealRooted.specializeLeft x + (sourceBlockPolarization n P) = + _root_.RealRooted.polarization n + (MvPolynomial.uniqueAlgEquiv ℂ (Fin 1) + (_root_.RealRooted.specializeLeft x P)) := by + let p : ℂ[X] := + (MvPolynomial.uniqueAlgEquiv ℂ (Fin 1)) + (_root_.RealRooted.specializeLeft x P) + have hpcoeff (k : ℕ) : + p.coeff k = MvPolynomial.eval x (sourceCoefficient P k) := by + dsimp only [p] + exact + coeff_uniqueAlgEquiv_specializeLeft_eq_eval_sourceCoefficient + P x k + have houtput (q : MvPolynomial τ ℂ) : + MvPolynomial.aeval + (Sum.elim (MvPolynomial.C ∘ x) MvPolynomial.X) + (rename (Sum.inl : τ → τ ⊕ Fin n) q) = + C (MvPolynomial.eval x q) := by + rw [MvPolynomial.aeval_rename] + change + MvPolynomial.aeval (MvPolynomial.C ∘ x) q = + C (MvPolynomial.eval x q) + induction q using MvPolynomial.induction_on with + | C c => simp + | add q r hq hr => simp [hq, hr] + | mul_X q i hq => simp [hq] + have hsource (q : MvPolynomial (Fin n) ℂ) : + MvPolynomial.aeval + (Sum.elim (MvPolynomial.C ∘ x) MvPolynomial.X) + (rename (Sum.inr : Fin n → τ ⊕ Fin n) q) = + q := by + rw [MvPolynomial.aeval_rename] + change MvPolynomial.aeval MvPolynomial.X q = q + exact MvPolynomial.aeval_X_left_apply q + change + _root_.RealRooted.specializeLeft x + (sourceBlockPolarization n P) = + _root_.RealRooted.polarization n p + unfold sourceBlockPolarization + unfold _root_.RealRooted.specializeLeft + rw [map_sum] + unfold _root_.RealRooted.polarization + unfold _root_.RealRooted.reducedPolarization + apply Finset.sum_congr rfl + intro k hk + rw [map_mul, map_mul, MvPolynomial.aeval_C, + MvPolynomial.algebraMap_eq, houtput, hsource] + have hbinom : + (_root_.RealRooted.binomialUnlift n p).coeff k = + p.coeff k / (n.choose k : ℂ) := by + unfold _root_.RealRooted.binomialUnlift + rw [Polynomial.finsetSum_coeff, Finset.sum_eq_single k] + · simp only [Polynomial.coeff_monomial_same] + · intro j hj hjk + simp [Polynomial.coeff_monomial, hjk] + · intro hknot + exact (hknot hk).elim + rw [hbinom, hpcoeff] + simp only [div_eq_mul_inv, map_mul] + ring + /-- Extracting a source coefficient commutes with a finite sum. -/ theorem sourceCoefficient_sum {τ ι : Type*} (s : Finset ι) (f : ι → MvPolynomial (τ ⊕ Fin 1) ℂ) (k : ℕ) : From 72615fbfb88f528c0950885f9819b350e18ad671 Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Mon, 3 Aug 2026 21:52:26 +0000 Subject: [PATCH 65/81] Golf specialization bridge plumbing --- .../Applications/DegreeBoxPolarization.lean | 12 ++++-------- 1 file changed, 4 insertions(+), 8 deletions(-) diff --git a/RealRooted/BorceaBranden/Applications/DegreeBoxPolarization.lean b/RealRooted/BorceaBranden/Applications/DegreeBoxPolarization.lean index ea821dc58..7d710808b 100644 --- a/RealRooted/BorceaBranden/Applications/DegreeBoxPolarization.lean +++ b/RealRooted/BorceaBranden/Applications/DegreeBoxPolarization.lean @@ -180,11 +180,8 @@ theorem specializeLeft_sourceBlockPolarization (MvPolynomial.uniqueAlgEquiv ℂ (Fin 1)) (_root_.RealRooted.specializeLeft x P) have hpcoeff (k : ℕ) : - p.coeff k = MvPolynomial.eval x (sourceCoefficient P k) := by - dsimp only [p] - exact - coeff_uniqueAlgEquiv_specializeLeft_eq_eval_sourceCoefficient - P x k + p.coeff k = MvPolynomial.eval x (sourceCoefficient P k) := + coeff_uniqueAlgEquiv_specializeLeft_eq_eval_sourceCoefficient P x k have houtput (q : MvPolynomial τ ℂ) : MvPolynomial.aeval (Sum.elim (MvPolynomial.C ∘ x) MvPolynomial.X) @@ -210,11 +207,10 @@ theorem specializeLeft_sourceBlockPolarization _root_.RealRooted.specializeLeft x (sourceBlockPolarization n P) = _root_.RealRooted.polarization n p - unfold sourceBlockPolarization - unfold _root_.RealRooted.specializeLeft + unfold sourceBlockPolarization _root_.RealRooted.specializeLeft rw [map_sum] unfold _root_.RealRooted.polarization - unfold _root_.RealRooted.reducedPolarization + _root_.RealRooted.reducedPolarization apply Finset.sum_congr rfl intro k hk rw [map_mul, map_mul, MvPolynomial.aeval_C, From 717ad290bcecd5b51102a389bf88c7253f0a71d4 Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Mon, 3 Aug 2026 21:59:54 +0000 Subject: [PATCH 66/81] Bound source degree after specialization --- RealRooted/MultivariateStability.lean | 76 +++++++++++++++++++++++++++ 1 file changed, 76 insertions(+) diff --git a/RealRooted/MultivariateStability.lean b/RealRooted/MultivariateStability.lean index 333211e8f..f814d9947 100644 --- a/RealRooted/MultivariateStability.lean +++ b/RealRooted/MultivariateStability.lean @@ -1,7 +1,9 @@ import Mathlib.Algebra.MvPolynomial.Eval +import Mathlib.Algebra.MvPolynomial.Equiv import Mathlib.Algebra.MvPolynomial.Funext import Mathlib.Algebra.MvPolynomial.Rename import Mathlib.Algebra.Polynomial.Eval.Coeff +import Mathlib.Algebra.Polynomial.Eval.Degree import Mathlib.Algebra.Polynomial.Splits import Mathlib.Data.Complex.Basic import Mathlib.Analysis.Complex.UpperHalfPlane.Basic @@ -489,6 +491,80 @@ theorem eval_specializeLeft {sigma tau : Type*} (x : sigma → ℂ) ext i cases i <;> simp +/-- Specializing one variable block cannot increase the degree in the +remaining singleton block. -/ +theorem natDegree_uniqueAlgEquiv_specializeLeft_le_degreeOf + {τ : Type*} (x : τ → ℂ) + (P : MvPolynomial (τ ⊕ Fin 1) ℂ) : + (MvPolynomial.uniqueAlgEquiv ℂ (Fin 1) + (specializeLeft x P)).natDegree ≤ + P.degreeOf (Sum.inr default) := by + let e : τ ⊕ Fin 1 ≃ Option τ := + { toFun := fun s => + match s with + | Sum.inl i => some i + | Sum.inr _ => none + invFun := fun o => + match o with + | some i => Sum.inl i + | none => Sum.inr default + left_inv := by + rintro (i | i) + · rfl + · exact congrArg Sum.inr (Subsingleton.elim default i) + right_inv := by + intro o + cases o <;> rfl } + let Q : MvPolynomial (Option τ) ℂ := + MvPolynomial.rename e P + have hQdeg : + (MvPolynomial.optionEquivLeft ℂ τ Q).natDegree = + P.degreeOf (Sum.inr default) := by + rw [MvPolynomial.natDegree_optionEquivLeft] + dsimp [Q] + simpa [e] using + (MvPolynomial.degreeOf_rename_of_injective + (p := P) e.injective (Sum.inr default)) + have hpoly : + MvPolynomial.uniqueAlgEquiv ℂ (Fin 1) + (specializeLeft x P) = + Polynomial.map (MvPolynomial.eval x) + (MvPolynomial.optionEquivLeft ℂ τ Q) := by + apply Polynomial.funext + intro y + change Polynomial.eval₂ (RingHom.id ℂ) y + (MvPolynomial.uniqueAlgEquiv ℂ (Fin 1) + (specializeLeft x P)) = + Polynomial.eval y + (Polynomial.map (MvPolynomial.eval x) + (MvPolynomial.optionEquivLeft ℂ τ Q)) + rw [MvPolynomial.eval₂_const_uniqueAlgEquiv] + change MvPolynomial.eval (fun _ : Fin 1 => y) + (specializeLeft x P) = _ + rw [eval_specializeLeft] + calc + MvPolynomial.eval (Sum.elim x fun _ => y) P = + MvPolynomial.eval + (fun o => Option.elim o y x) Q := by + dsimp [Q] + rw [MvPolynomial.eval_rename] + apply congrArg (fun z => MvPolynomial.eval z P) + funext i + cases i <;> rfl + _ = Polynomial.eval y + (Polynomial.map (MvPolynomial.eval x) + (MvPolynomial.optionEquivLeft ℂ τ Q)) := + MvPolynomial.optionEquivLeft_elim_eval x y Q + calc + (MvPolynomial.uniqueAlgEquiv ℂ (Fin 1) + (specializeLeft x P)).natDegree = + (Polynomial.map (MvPolynomial.eval x) + (MvPolynomial.optionEquivLeft ℂ τ Q)).natDegree := + congrArg (fun p : ℂ[X] => p.natDegree) hpoly + _ ≤ (MvPolynomial.optionEquivLeft ℂ τ Q).natDegree := + Polynomial.natDegree_map_le + _ = P.degreeOf (Sum.inr default) := hQdeg + /-- Specializing the left block inside its regions preserves stability in the right coordinate regions. -/ theorem MvStableIn.specializeLeft From 096a3f3a20143c628c744de683b560133d030fbf Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Mon, 3 Aug 2026 22:05:00 +0000 Subject: [PATCH 67/81] Fix specialization degree proof arguments --- RealRooted/MultivariateStability.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/RealRooted/MultivariateStability.lean b/RealRooted/MultivariateStability.lean index f814d9947..1eec007ea 100644 --- a/RealRooted/MultivariateStability.lean +++ b/RealRooted/MultivariateStability.lean @@ -554,7 +554,7 @@ theorem natDegree_uniqueAlgEquiv_specializeLeft_le_degreeOf _ = Polynomial.eval y (Polynomial.map (MvPolynomial.eval x) (MvPolynomial.optionEquivLeft ℂ τ Q)) := - MvPolynomial.optionEquivLeft_elim_eval x y Q + MvPolynomial.optionEquivLeft_elim_eval ℂ τ x y Q calc (MvPolynomial.uniqueAlgEquiv ℂ (Fin 1) (specializeLeft x P)).natDegree = From 52e409314b32a0612810075bfb2502f9af9f5df3 Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Mon, 3 Aug 2026 22:07:19 +0000 Subject: [PATCH 68/81] Golf specialization degree bound --- RealRooted/MultivariateStability.lean | 14 +++----------- 1 file changed, 3 insertions(+), 11 deletions(-) diff --git a/RealRooted/MultivariateStability.lean b/RealRooted/MultivariateStability.lean index 1eec007ea..be4d1c764 100644 --- a/RealRooted/MultivariateStability.lean +++ b/RealRooted/MultivariateStability.lean @@ -521,8 +521,7 @@ theorem natDegree_uniqueAlgEquiv_specializeLeft_le_degreeOf (MvPolynomial.optionEquivLeft ℂ τ Q).natDegree = P.degreeOf (Sum.inr default) := by rw [MvPolynomial.natDegree_optionEquivLeft] - dsimp [Q] - simpa [e] using + simpa [Q, e] using (MvPolynomial.degreeOf_rename_of_injective (p := P) e.injective (Sum.inr default)) have hpoly : @@ -555,15 +554,8 @@ theorem natDegree_uniqueAlgEquiv_specializeLeft_le_degreeOf (Polynomial.map (MvPolynomial.eval x) (MvPolynomial.optionEquivLeft ℂ τ Q)) := MvPolynomial.optionEquivLeft_elim_eval ℂ τ x y Q - calc - (MvPolynomial.uniqueAlgEquiv ℂ (Fin 1) - (specializeLeft x P)).natDegree = - (Polynomial.map (MvPolynomial.eval x) - (MvPolynomial.optionEquivLeft ℂ τ Q)).natDegree := - congrArg (fun p : ℂ[X] => p.natDegree) hpoly - _ ≤ (MvPolynomial.optionEquivLeft ℂ τ Q).natDegree := - Polynomial.natDegree_map_le - _ = P.degreeOf (Sum.inr default) := hQdeg + rw [hpoly, ← hQdeg] + exact Polynomial.natDegree_map_le /-- Specializing the left block inside its regions preserves stability in the right coordinate regions. -/ From 8e60f2e305b6da505bbfe3efa2570ac0b4e4b307 Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Mon, 3 Aug 2026 22:16:14 +0000 Subject: [PATCH 69/81] Preserve stability under source polarization --- .../Applications/DegreeBoxPolarization.lean | 55 +++++++++++++++++++ 1 file changed, 55 insertions(+) diff --git a/RealRooted/BorceaBranden/Applications/DegreeBoxPolarization.lean b/RealRooted/BorceaBranden/Applications/DegreeBoxPolarization.lean index 7d710808b..799139d46 100644 --- a/RealRooted/BorceaBranden/Applications/DegreeBoxPolarization.lean +++ b/RealRooted/BorceaBranden/Applications/DegreeBoxPolarization.lean @@ -229,6 +229,61 @@ theorem specializeLeft_sourceBlockPolarization simp only [div_eq_mul_inv, map_mul] ring +/- Borcea--Branden, arXiv:0809.0401, Proposition 2.4. Apply upper-half-plane +polarization stability fiberwise after specializing the output block. The +ambient source-degree cap remains `n` after specialization. -/ +theorem mvUpperHalfPlaneStable_sourceBlockPolarization + {τ : Type*} {n : ℕ} + {P : MvPolynomial (τ ⊕ Fin 1) ℂ} + (hdeg : P.degreeOf (Sum.inr default) ≤ n) + (hstable : _root_.RealRooted.MvUpperHalfPlaneStable P) : + _root_.RealRooted.MvUpperHalfPlaneStable + (sourceBlockPolarization n P) := by + intro z hz + let x : τ → ℂ := fun i => z (Sum.inl i) + let y : Fin n → ℂ := fun i => z (Sum.inr i) + let p : ℂ[X] := + MvPolynomial.uniqueAlgEquiv ℂ (Fin 1) + (_root_.RealRooted.specializeLeft x P) + have hx : ∀ i, 0 < (x i).im := + fun i => hz (Sum.inl i) + have hy : ∀ i, 0 < (y i).im := + fun i => hz (Sum.inr i) + have hpdeg : p.natDegree ≤ n := by + exact + (_root_.RealRooted.natDegree_uniqueAlgEquiv_specializeLeft_le_degreeOf + x P).trans hdeg + have hspecial : + _root_.RealRooted.MvUpperHalfPlaneStable + (_root_.RealRooted.specializeLeft x P) := + hstable.specializeLeft hx + have hpstable : + ∀ w : ℂ, 0 < w.im → p.eval w ≠ 0 := by + intro w hw + change + Polynomial.eval₂ (RingHom.id ℂ) w + (MvPolynomial.uniqueAlgEquiv ℂ (Fin 1) + (_root_.RealRooted.specializeLeft x P)) ≠ 0 + rw [MvPolynomial.eval₂_const_uniqueAlgEquiv] + exact hspecial (fun _ => w) (fun _ => hw) + have hpolar : + _root_.RealRooted.MvUpperHalfPlaneStable + (_root_.RealRooted.polarization n p) := + _root_.RealRooted.mvUpperHalfPlaneStable_polarization + hpdeg hpstable + have hfiber : + _root_.RealRooted.MvUpperHalfPlaneStable + (_root_.RealRooted.specializeLeft x + (sourceBlockPolarization n P)) := by + rw [specializeLeft_sourceBlockPolarization] + exact hpolar + have hnonzero := hfiber y hy + rw [_root_.RealRooted.eval_specializeLeft] at hnonzero + have hxy : Sum.elim x y = z := by + funext i + cases i <;> rfl + simpa only [hxy] using hnonzero + /-- Extracting a source coefficient commutes with a finite sum. -/ theorem sourceCoefficient_sum {τ ι : Type*} (s : Finset ι) (f : ι → MvPolynomial (τ ⊕ Fin 1) ℂ) (k : ℕ) : From 5b7fd6affea556ea0cc04458a6a018f9ddb0c127 Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Mon, 3 Aug 2026 22:19:46 +0000 Subject: [PATCH 70/81] Bound algebraic symbol source degree --- .../BorceaBranden/FiniteSymbolDegree.lean | 65 +++++++++++++++++++ 1 file changed, 65 insertions(+) diff --git a/RealRooted/BorceaBranden/FiniteSymbolDegree.lean b/RealRooted/BorceaBranden/FiniteSymbolDegree.lean index 8de10c4bc..4d6711393 100644 --- a/RealRooted/BorceaBranden/FiniteSymbolDegree.lean +++ b/RealRooted/BorceaBranden/FiniteSymbolDegree.lean @@ -28,6 +28,71 @@ variable {sigma tau R : Type*} [CommSemiring R] [Fintype sigma] /-- The finite algebraic symbol for the multiaffine degree box has degree at most one in every source coordinate. No degree bound is imposed on the target variables. -/ +/- Borcea--Branden, arXiv:0809.0401, Section 1.1. In each summand of +`G_T(z,w)`, source variable `w_i` has exponent `κ i - α i`, hence at most +`κ i`; the renamed operator value uses only the output-variable block. -/ +theorem degreeOf_algebraicSymbol_inr_le + (κ : sigma → ℕ) + (T : degreeOfLE sigma R κ →ₗ[R] MvPolynomial tau R) + (i : sigma) : + (algebraicSymbol κ T).degreeOf (Sum.inr i) ≤ κ i := by + classical + rcases subsingleton_or_nontrivial R with hR | hR + · letI := hR + rw [Subsingleton.elim (algebraicSymbol κ T) 0] + simp + · letI := hR + rw [algebraicSymbol_eq_sum] + refine (degreeOf_sum_le (Sum.inr i) Finset.univ fun m => + C (boxChoose κ m.1 : R) * + rename (Sum.inl : tau → tau ⊕ sigma) + (T (basisDegreeOfLE κ m)) * + rightComplementMonomial κ m.1).trans ?_ + apply Finset.sup_le + intro m hm + have hrename : + (rename (Sum.inl : tau → tau ⊕ sigma) + (T (basisDegreeOfLE κ m))).degreeOf (Sum.inr i) = 0 := by + apply Nat.le_zero.mp + rw [degreeOf_le_iff] + intro d hd + apply Nat.le_zero.mpr + by_contra hdi + have hmem : Sum.inr i ∈ + (rename (Sum.inl : tau → tau ⊕ sigma) + (T (basisDegreeOfLE κ m))).vars := by + rw [mem_vars_iff_mem_support] + exact ⟨d, hd, Finsupp.mem_support_iff.mpr hdi⟩ + obtain ⟨j, _hj, hji⟩ := mem_vars_rename Sum.inl _ hmem + exact Sum.inl_ne_inr hji + have hleft : + (C (boxChoose κ m.1 : R) * + rename (Sum.inl : tau → tau ⊕ sigma) + (T (basisDegreeOfLE κ m))).degreeOf (Sum.inr i) ≤ 0 := by + exact (degreeOf_C_mul_le _ _ _).trans_eq hrename + have hright : + (rightComplementMonomial (R := R) (τ := tau) + κ m.1).degreeOf (Sum.inr i) ≤ κ i := by + rw [rightComplementMonomial_eq_prod] + refine (degreeOf_prod_le (Sum.inr i) Finset.univ fun j => + X (Sum.inr j) ^ (κ j - m.1 j)).trans ?_ + calc + ∑ j : sigma, + (X (Sum.inr j) ^ (κ j - m.1 j) : + MvPolynomial (tau ⊕ sigma) R).degreeOf (Sum.inr i) = + κ i - m.1 i := by + rw [Finset.sum_eq_single i] + · simp + · intro j hj hji + rw [degreeOf_X_pow_of_ne] + intro hij + exact hji (Sum.inr_injective hij).symm + · simp + _ ≤ κ i := Nat.sub_le _ _ + exact (degreeOf_mul_le _ _ _).trans + ((Nat.add_le_add hleft hright).trans_eq + (Nat.zero_add (κ i))) + theorem degreeOf_algebraicSymbol_one_inr_le (T : degreeOfLE sigma R (fun _ => 1) →ₗ[R] MvPolynomial tau R) (i : sigma) : From 9b5367fb38d9749f257bd5a364bdf35f5b43d849 Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Mon, 3 Aug 2026 22:21:24 +0000 Subject: [PATCH 71/81] Deduplicate algebraic symbol degree bounds --- .../BorceaBranden/FiniteSymbolDegree.lean | 60 +------------------ 1 file changed, 2 insertions(+), 58 deletions(-) diff --git a/RealRooted/BorceaBranden/FiniteSymbolDegree.lean b/RealRooted/BorceaBranden/FiniteSymbolDegree.lean index 4d6711393..338db9cfe 100644 --- a/RealRooted/BorceaBranden/FiniteSymbolDegree.lean +++ b/RealRooted/BorceaBranden/FiniteSymbolDegree.lean @@ -49,7 +49,7 @@ theorem degreeOf_algebraicSymbol_inr_le (T (basisDegreeOfLE κ m)) * rightComplementMonomial κ m.1).trans ?_ apply Finset.sup_le - intro m hm + intro m _ have hrename : (rename (Sum.inl : tau → tau ⊕ sigma) (T (basisDegreeOfLE κ m))).degreeOf (Sum.inr i) = 0 := by @@ -97,63 +97,7 @@ theorem degreeOf_algebraicSymbol_one_inr_le (T : degreeOfLE sigma R (fun _ => 1) →ₗ[R] MvPolynomial tau R) (i : sigma) : (algebraicSymbol (fun _ : sigma => 1) T).degreeOf (Sum.inr i) ≤ 1 := by - classical - rcases subsingleton_or_nontrivial R with hR | hR - · letI := hR - rw [Subsingleton.elim (algebraicSymbol (fun _ : sigma => 1) T) 0] - simp - · letI := hR - rw [algebraicSymbol_eq_sum] - refine (degreeOf_sum_le (Sum.inr i) Finset.univ fun m => - C (boxChoose (fun _ : sigma => 1) m.1 : R) * - rename (Sum.inl : tau → tau ⊕ sigma) - (T (basisDegreeOfLE (fun _ : sigma => 1) m)) * - rightComplementMonomial (fun _ : sigma => 1) m.1).trans ?_ - apply Finset.sup_le - intro m hm - have hrename : - (rename (Sum.inl : tau → tau ⊕ sigma) - (T (basisDegreeOfLE (fun _ : sigma => 1) m))).degreeOf - (Sum.inr i) = 0 := by - apply Nat.le_zero.mp - rw [degreeOf_le_iff] - intro d hd - apply Nat.le_zero.mpr - by_contra hdi - have hmem : Sum.inr i ∈ - (rename (Sum.inl : tau → tau ⊕ sigma) - (T (basisDegreeOfLE (fun _ : sigma => 1) m))).vars := by - rw [mem_vars_iff_mem_support] - exact ⟨d, hd, Finsupp.mem_support_iff.mpr hdi⟩ - obtain ⟨j, _hj, hji⟩ := mem_vars_rename Sum.inl _ hmem - exact Sum.inl_ne_inr hji - have hleft : - (C (boxChoose (fun _ : sigma => 1) m.1 : R) * - rename (Sum.inl : tau → tau ⊕ sigma) - (T (basisDegreeOfLE (fun _ : sigma => 1) m))).degreeOf - (Sum.inr i) ≤ 0 := by - exact (degreeOf_C_mul_le _ _ _).trans_eq hrename - have hright : - (rightComplementMonomial (R := R) (τ := tau) - (fun _ : sigma => 1) m.1).degreeOf (Sum.inr i) ≤ 1 := by - rw [rightComplementMonomial_eq_prod] - refine (degreeOf_prod_le (Sum.inr i) Finset.univ fun j => - X (Sum.inr j) ^ (1 - m.1 j)).trans ?_ - calc - ∑ j : sigma, - (X (Sum.inr j) ^ (1 - m.1 j) : - MvPolynomial (tau ⊕ sigma) R).degreeOf (Sum.inr i) = - 1 - m.1 i := by - rw [Finset.sum_eq_single i] - · simp - · intro j hj hji - rw [degreeOf_X_pow_of_ne] - intro hij - exact hji (Sum.inr_injective hij).symm - · simp - _ ≤ 1 := Nat.sub_le _ _ - exact (degreeOf_mul_le _ _ _).trans - ((Nat.add_le_add hleft hright).trans_eq (Nat.zero_add 1)) + exact degreeOf_algebraicSymbol_inr_le (fun _ : sigma => 1) T i end From f9e539f9d2c74885b2635ae77437623eb99efaa6 Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Mon, 3 Aug 2026 22:23:14 +0000 Subject: [PATCH 72/81] Transfer finite symbol stability through polarization --- .../Applications/DegreeBoxPolarization.lean | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) diff --git a/RealRooted/BorceaBranden/Applications/DegreeBoxPolarization.lean b/RealRooted/BorceaBranden/Applications/DegreeBoxPolarization.lean index 799139d46..67654434e 100644 --- a/RealRooted/BorceaBranden/Applications/DegreeBoxPolarization.lean +++ b/RealRooted/BorceaBranden/Applications/DegreeBoxPolarization.lean @@ -576,6 +576,25 @@ theorem algebraicSymbol_sourcePolarizedOperator /-- Termwise form of the source-polarized algebraic symbol after identifying all polarized source variables. -/ +/-- Borcea--Brändén, Lemma 2.5 and Proposition 2.4: stability of a finite +algebraic symbol is preserved when its single source variable is polarized +into a multiaffine source block. -/ +theorem mvUpperHalfPlaneStable_algebraicSymbol_sourcePolarizedOperator + {τ : Type*} (n : ℕ) + (T : degreeOfLE (Fin 1) ℂ (fun _ => n) →ₗ[ℂ] + MvPolynomial τ ℂ) + (hstable : + MvUpperHalfPlaneStable + (algebraicSymbol (fun _ : Fin 1 => n) T)) : + MvUpperHalfPlaneStable + (algebraicSymbol (fun _ : Fin n => 1) + (sourcePolarizedOperator n T)) := by + rw [algebraicSymbol_sourcePolarizedOperator] + exact MvPolynomial.mvUpperHalfPlaneStable_sourceBlockPolarization + (MvPolynomial.degreeOf_algebraicSymbol_inr_le + (fun _ : Fin 1 => n) T default) + hstable + theorem rename_algebraicSymbol_sourcePolarizedOperator_eq_sum {τ : Type*} (n : ℕ) (T : degreeOfLE (Fin 1) ℂ (fun _ => n) →ₗ[ℂ] From fe13bc227b1910366c329b5c9c606cc7103d8eb4 Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Mon, 3 Aug 2026 22:28:38 +0000 Subject: [PATCH 73/81] Document Jensen backend obstruction --- RealRooted/Tactic/PFBidiagonal.lean | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/RealRooted/Tactic/PFBidiagonal.lean b/RealRooted/Tactic/PFBidiagonal.lean index da5936bf2..535a48339 100644 --- a/RealRooted/Tactic/PFBidiagonal.lean +++ b/RealRooted/Tactic/PFBidiagonal.lean @@ -371,6 +371,18 @@ def BidiagonalJensenPencilCertificate /-- Backend theorem statement: a valid finite Jensen-pencil certificate implies that the corresponding coefficient-bidiagonal operator preserves PF polynomials up to degree `d`. -/ +/- This is deliberately an explicit backend assumption, not a proved theorem. +The certificate above tests only the real pencil parameter `lam ≥ 0`; it does +not imply upper-half-plane stability of the genuine bivariate affine symbol +required by Borcea--Branden, arXiv:0809.0401, Theorem 1.1. Issue #240 records +the degree-two obstruction `alpha = (3, 2, 1)`, `beta = (4, 1 / 2, 0)`: every +nonnegative Jensen pencil is PF, while the associated operator sends +`(1 - 2 * X)^2` to `3 - 4 * X + 2 * X^2`, whose discriminant is negative. +Garloff--Wagner, Theorem 12(b), preserves an already supplied proper-position +orientation and does not infer it from this one-sided pencil. Downstream +wrappers remain sound because they require a proof of this proposition as an +explicit argument; they must not manufacture it from affine-symbol stability. +-/ def jensenPencilBidiagonalPreserverStatement : Prop := ∀ {alpha beta : ℕ → ℝ} {d : ℕ}, BidiagonalJensenPencilCertificate alpha beta d → From 643e4aa04549d2352ed904769d30c163e4c386d5 Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Mon, 3 Aug 2026 22:31:50 +0000 Subject: [PATCH 74/81] Clean up finite symbol documentation --- .../Applications/DegreeBoxPolarization.lean | 14 +++++++------- RealRooted/Tactic/PFBidiagonal.lean | 5 +++-- 2 files changed, 10 insertions(+), 9 deletions(-) diff --git a/RealRooted/BorceaBranden/Applications/DegreeBoxPolarization.lean b/RealRooted/BorceaBranden/Applications/DegreeBoxPolarization.lean index 67654434e..c72e6979d 100644 --- a/RealRooted/BorceaBranden/Applications/DegreeBoxPolarization.lean +++ b/RealRooted/BorceaBranden/Applications/DegreeBoxPolarization.lean @@ -574,8 +574,6 @@ theorem algebraicSymbol_sourcePolarizedOperator (fun k => T (basisDegreeOfLE (R := ℂ) (fun _ : Fin 1 => n) (finOneDegreeIndex n k))) -/-- Termwise form of the source-polarized algebraic symbol after identifying -all polarized source variables. -/ /-- Borcea--Brändén, Lemma 2.5 and Proposition 2.4: stability of a finite algebraic symbol is preserved when its single source variable is polarized into a multiaffine source block. -/ @@ -589,12 +587,14 @@ theorem mvUpperHalfPlaneStable_algebraicSymbol_sourcePolarizedOperator MvUpperHalfPlaneStable (algebraicSymbol (fun _ : Fin n => 1) (sourcePolarizedOperator n T)) := by - rw [algebraicSymbol_sourcePolarizedOperator] - exact MvPolynomial.mvUpperHalfPlaneStable_sourceBlockPolarization - (MvPolynomial.degreeOf_algebraicSymbol_inr_le - (fun _ : Fin 1 => n) T default) - hstable + simpa only [algebraicSymbol_sourcePolarizedOperator] using + MvPolynomial.mvUpperHalfPlaneStable_sourceBlockPolarization + (MvPolynomial.degreeOf_algebraicSymbol_inr_le + (fun _ : Fin 1 => n) T default) + hstable +/-- Termwise form of the source-polarized algebraic symbol after identifying +all polarized source variables. -/ theorem rename_algebraicSymbol_sourcePolarizedOperator_eq_sum {τ : Type*} (n : ℕ) (T : degreeOfLE (Fin 1) ℂ (fun _ => n) →ₗ[ℂ] diff --git a/RealRooted/Tactic/PFBidiagonal.lean b/RealRooted/Tactic/PFBidiagonal.lean index 535a48339..7c7f3de06 100644 --- a/RealRooted/Tactic/PFBidiagonal.lean +++ b/RealRooted/Tactic/PFBidiagonal.lean @@ -370,8 +370,9 @@ def BidiagonalJensenPencilCertificate /-- Backend theorem statement: a valid finite Jensen-pencil certificate implies that the corresponding coefficient-bidiagonal operator preserves PF -polynomials up to degree `d`. -/ -/- This is deliberately an explicit backend assumption, not a proved theorem. +polynomials up to degree `d`. + +This is deliberately an explicit backend assumption, not a proved theorem. The certificate above tests only the real pencil parameter `lam ≥ 0`; it does not imply upper-half-plane stability of the genuine bivariate affine symbol required by Borcea--Branden, arXiv:0809.0401, Theorem 1.1. Issue #240 records From f18c2fefd3babe2d5a3f03aadf0d3d8339c91b74 Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Mon, 3 Aug 2026 22:38:27 +0000 Subject: [PATCH 75/81] Document PF-specific Jensen source gap --- RealRooted/Tactic/PFBidiagonal.lean | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/RealRooted/Tactic/PFBidiagonal.lean b/RealRooted/Tactic/PFBidiagonal.lean index 7c7f3de06..03f5902ab 100644 --- a/RealRooted/Tactic/PFBidiagonal.lean +++ b/RealRooted/Tactic/PFBidiagonal.lean @@ -380,9 +380,13 @@ the degree-two obstruction `alpha = (3, 2, 1)`, `beta = (4, 1 / 2, 0)`: every nonnegative Jensen pencil is PF, while the associated operator sends `(1 - 2 * X)^2` to `3 - 4 * X + 2 * X^2`, whose discriminant is negative. Garloff--Wagner, Theorem 12(b), preserves an already supplied proper-position -orientation and does not infer it from this one-sided pencil. Downstream -wrappers remain sound because they require a proof of this proposition as an -explicit argument; they must not manufacture it from affine-symbol stability. +orientation and does not infer it from this one-sided pencil. Brändén, +arXiv:math/0403364, Theorem 3.6, is PF-specific but requires fiberwise +real-rootedness of a differential symbol, strict interlacing of `phi(1)` and +`phi(X)`, and exact degree growth; the current certificate does not imply these +hypotheses. Downstream wrappers remain sound because they require a proof of +this proposition as an explicit argument; they must not manufacture it from +either source theorem. -/ def jensenPencilBidiagonalPreserverStatement : Prop := ∀ {alpha beta : ℕ → ℝ} {d : ℕ}, From 647cf8a851047a04b72c6b0df7da0a48d86fb18b Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Mon, 3 Aug 2026 23:20:01 +0000 Subject: [PATCH 76/81] Fix degree-box polarization elaboration --- .../Applications/DegreeBoxPolarization.lean | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/RealRooted/BorceaBranden/Applications/DegreeBoxPolarization.lean b/RealRooted/BorceaBranden/Applications/DegreeBoxPolarization.lean index c72e6979d..88212c739 100644 --- a/RealRooted/BorceaBranden/Applications/DegreeBoxPolarization.lean +++ b/RealRooted/BorceaBranden/Applications/DegreeBoxPolarization.lean @@ -1,4 +1,5 @@ import RealRooted.BorceaBranden.FiniteSymbolBasis +import RealRooted.BorceaBranden.FiniteSymbolDegree import RealRooted.Polarization /-! @@ -176,7 +177,7 @@ theorem specializeLeft_sourceBlockPolarization _root_.RealRooted.polarization n (MvPolynomial.uniqueAlgEquiv ℂ (Fin 1) (_root_.RealRooted.specializeLeft x P)) := by - let p : ℂ[X] := + let p : Polynomial ℂ := (MvPolynomial.uniqueAlgEquiv ℂ (Fin 1)) (_root_.RealRooted.specializeLeft x P) have hpcoeff (k : ℕ) : @@ -193,8 +194,10 @@ theorem specializeLeft_sourceBlockPolarization C (MvPolynomial.eval x q) induction q using MvPolynomial.induction_on with | C c => simp - | add q r hq hr => simp [hq, hr] - | mul_X q i hq => simp [hq] + | add q r hq hr => rw [map_add, hq, hr, map_add] + | mul_X q i hq => + rw [map_mul, MvPolynomial.aeval_X, hq, map_mul, + MvPolynomial.eval_X] have hsource (q : MvPolynomial (Fin n) ℂ) : MvPolynomial.aeval (Sum.elim (MvPolynomial.C ∘ x) MvPolynomial.X) @@ -242,7 +245,7 @@ theorem mvUpperHalfPlaneStable_sourceBlockPolarization intro z hz let x : τ → ℂ := fun i => z (Sum.inl i) let y : Fin n → ℂ := fun i => z (Sum.inr i) - let p : ℂ[X] := + let p : Polynomial ℂ := MvPolynomial.uniqueAlgEquiv ℂ (Fin 1) (_root_.RealRooted.specializeLeft x P) have hx : ∀ i, 0 < (x i).im := From f8d2c818db0bfdbeec53541bdeff9655f48607a2 Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Mon, 3 Aug 2026 23:29:44 +0000 Subject: [PATCH 77/81] Close source specialization homomorphism goals --- .../BorceaBranden/Applications/DegreeBoxPolarization.lean | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/RealRooted/BorceaBranden/Applications/DegreeBoxPolarization.lean b/RealRooted/BorceaBranden/Applications/DegreeBoxPolarization.lean index 88212c739..a215a09da 100644 --- a/RealRooted/BorceaBranden/Applications/DegreeBoxPolarization.lean +++ b/RealRooted/BorceaBranden/Applications/DegreeBoxPolarization.lean @@ -194,10 +194,14 @@ theorem specializeLeft_sourceBlockPolarization C (MvPolynomial.eval x q) induction q using MvPolynomial.induction_on with | C c => simp - | add q r hq hr => rw [map_add, hq, hr, map_add] + | add q r hq hr => + rw [map_add, hq, hr, map_add] + exact (map_add MvPolynomial.C _ _).symm | mul_X q i hq => rw [map_mul, MvPolynomial.aeval_X, hq, map_mul, MvPolynomial.eval_X] + simpa only [Function.comp_apply] using + (map_mul MvPolynomial.C (MvPolynomial.eval x q) (x i)).symm have hsource (q : MvPolynomial (Fin n) ℂ) : MvPolynomial.aeval (Sum.elim (MvPolynomial.C ∘ x) MvPolynomial.X) From d0783bcac82477185bf3d78fdb034b37145df194 Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Tue, 4 Aug 2026 00:16:13 +0000 Subject: [PATCH 78/81] Prove finite-symbol sufficiency for Fin 1 degree boxes --- .../Applications/DegreeBoxPolarization.lean | 48 +++++++++++++++++++ 1 file changed, 48 insertions(+) diff --git a/RealRooted/BorceaBranden/Applications/DegreeBoxPolarization.lean b/RealRooted/BorceaBranden/Applications/DegreeBoxPolarization.lean index a215a09da..5d3b2fb21 100644 --- a/RealRooted/BorceaBranden/Applications/DegreeBoxPolarization.lean +++ b/RealRooted/BorceaBranden/Applications/DegreeBoxPolarization.lean @@ -1,5 +1,6 @@ import RealRooted.BorceaBranden.FiniteSymbolBasis import RealRooted.BorceaBranden.FiniteSymbolDegree +import RealRooted.BorceaBranden.FiniteSymbolPreserver import RealRooted.Polarization /-! @@ -99,6 +100,53 @@ theorem sum_degreeOneExponent_degreeFunction end +/-- Finite-symbol sufficiency for a one-variable source degree box. + +This is the source-side specialization of Borcea--Branden, proof of Theorem 1.1, +using equations (2.1)--(2.2), Proposition 2.4, and Lemma 2.5 (Section 2.2, +pp. 10--12). The conclusion is zero-aware because Lemma 2.2 permits the +operator value to vanish. -/ +theorem finiteSymbol_finOne_preserves_stability + {tau : Type*} (n : ℕ) + (T : MvPolynomial.degreeOfLE (Fin 1) ℂ (fun _ => n) →ₗ[ℂ] + MvPolynomial tau ℂ) + (hSymbol : MvUpperHalfPlaneStable + (MvPolynomial.algebraicSymbol (fun _ : Fin 1 => n) T)) + (f : MvPolynomial.degreeOfLE (Fin 1) ℂ (fun _ => n)) + (hf : MvUpperHalfPlaneStable f.1) : + MvUpperHalfPlaneStableOrZero (T f) := by + have hdegree : + (MvPolynomial.uniqueAlgEquiv ℂ (Fin 1) f.1).natDegree ≤ n := by + calc + (MvPolynomial.uniqueAlgEquiv ℂ (Fin 1) f.1).natDegree = + f.1.degreeOf default := by + simpa only [AlgEquiv.symm_apply_apply] using + (MvPolynomial.degreeOf_uniqueAlgEquiv_symm (σ := Fin 1) + (MvPolynomial.uniqueAlgEquiv ℂ (Fin 1) f.1)).symm + _ ≤ n := + (MvPolynomial.mem_degreeOfLE_iff_degreeOf f.1).mp f.2 default + have hunivariate : + ∀ w : ℂ, 0 < w.im → + (MvPolynomial.uniqueAlgEquiv ℂ (Fin 1) f.1).eval w ≠ 0 := by + intro w hw + change Polynomial.eval₂ (RingHom.id ℂ) w + (MvPolynomial.uniqueAlgEquiv ℂ (Fin 1) f.1) ≠ 0 + rw [MvPolynomial.eval₂_const_uniqueAlgEquiv] + exact hf (fun _ => w) (fun _ => hw) + have hpolarized : MvUpperHalfPlaneStable + (polarizationDegreeBoxLinearMap n f).1 := by + change MvUpperHalfPlaneStable + (polarization n (MvPolynomial.uniqueAlgEquiv ℂ (Fin 1) f.1)) + exact mvUpperHalfPlaneStable_polarization hdegree hunivariate + have hlifted := finiteSymbol_preserves_stability + (sourcePolarizedOperator n T) + (mvUpperHalfPlaneStable_algebraicSymbol_sourcePolarizedOperator + n T hSymbol) + (polarizationDegreeBoxLinearMap n f) hpolarized + simpa only [sourcePolarizedOperator, LinearMap.comp_apply, + diagonalProjectionDegreeBox_comp_polarizationDegreeBoxLinearMap] using + hlifted + end RealRooted.BorceaBranden namespace MvPolynomial From 7a7910d97da8d96acb320cdab66b6fb2e695306f Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Tue, 4 Aug 2026 00:30:07 +0000 Subject: [PATCH 79/81] Apply degree-box sufficiency to bidiagonal symbols --- .../Applications/BidiagonalSymbol.lean | 207 ++++++++++++++++++ 1 file changed, 207 insertions(+) diff --git a/RealRooted/BorceaBranden/Applications/BidiagonalSymbol.lean b/RealRooted/BorceaBranden/Applications/BidiagonalSymbol.lean index 201c2eeff..cdd041fc5 100644 --- a/RealRooted/BorceaBranden/Applications/BidiagonalSymbol.lean +++ b/RealRooted/BorceaBranden/Applications/BidiagonalSymbol.lean @@ -1,4 +1,5 @@ import RealRooted.BorceaBranden.Applications.UnivariateSymbol +import RealRooted.BorceaBranden.Applications.DegreeBoxPolarization import RealRooted.MultiplierSequence /-! @@ -46,4 +47,210 @@ theorem finiteAlgebraicSymbol_bidiagonalLinearMap (alpha beta : ℕ → ℝ) (d simp [bidiagonalLinearMap, Polynomial.X_pow_eq_monomial, diagonalOperator_monomial, Challenges.BorceaBranden.polynomialInFirstMv] +/-! ## Complex degree-box application -/ + +/-- Complex-linear extension of the real bidiagonal operator. -/ +def complexBidiagonalLinearMap (alpha beta : ℕ → ℝ) : + Polynomial ℂ →ₗ[ℂ] Polynomial ℂ where + toFun := fun p => + diagonalOperator (fun k => (alpha k : ℂ)) p + + Polynomial.X * diagonalOperator (fun k => (beta k : ℂ)) p + map_add' p q := by + simp only [diagonalOperator_add, mul_add] + abel + map_smul' c p := by + simp only [smul_eq_C_mul, diagonalOperator_C_mul] + simp [mul_comm] + ring + +/-- Regard a complex univariate polynomial as a bivariate polynomial in the +first variable. -/ +def complexPolynomialInFirstMv (p : ℂ[X]) : MvPolynomial (Fin 2) ℂ := + p.eval₂ (MvPolynomial.C : ℂ →+* MvPolynomial (Fin 2) ℂ) + (MvPolynomial.X (0 : Fin 2)) + +/-- Complex finite algebraic symbol of a complex-linear univariate operator. -/ +def complexFiniteAlgebraicSymbol (d : ℕ) (T : ℂ[X] →ₗ[ℂ] ℂ[X]) : + MvPolynomial (Fin 2) ℂ := + ∑ k ∈ Finset.range (d + 1), + MvPolynomial.C (Nat.choose d k : ℂ) * + complexPolynomialInFirstMv (T ((X : ℂ[X]) ^ k)) * + MvPolynomial.X (1 : Fin 2) ^ (d - k) + +/-- Restrict a complex univariate operator to the degree-`d` box. -/ +def complexUnivariateDegreeBoxOperator (d : ℕ) + (T : ℂ[X] →ₗ[ℂ] ℂ[X]) : + MvPolynomial.degreeOfLE (Fin 1) ℂ (fun _ => d) →ₗ[ℂ] + MvPolynomial (Fin 1) ℂ where + toFun p := + (MvPolynomial.uniqueAlgEquiv ℂ (Fin 1)).symm + (T (MvPolynomial.uniqueAlgEquiv ℂ (Fin 1) p.1)) + map_add' p q := by simp + map_smul' c p := by simp + +lemma rename_uniqueAlgEquiv_symm_eq_complexPolynomialInFirstMv (p : ℂ[X]) : + MvPolynomial.rename finOneSumToFinTwo + (MvPolynomial.rename (Sum.inl : Fin 1 → Fin 1 ⊕ Fin 1) + ((MvPolynomial.uniqueAlgEquiv ℂ (Fin 1)).symm p)) = + complexPolynomialInFirstMv p := by + induction p using Polynomial.induction_on' with + | add p q hp hq => + simpa only [map_add, complexPolynomialInFirstMv, Polynomial.eval₂_add] using + congrArg₂ (· + ·) hp hq + | monomial n a => + have h := MvPolynomial.uniqueAlgEquiv_symm_monomial + (R := ℂ) (σ := Fin 1) (d := Finsupp.single 0 n) (r := a) + rw [show (MvPolynomial.uniqueAlgEquiv ℂ (Fin 1)).symm + (Polynomial.monomial n a) = + MvPolynomial.monomial (Finsupp.single 0 n) a by simpa using h] + simp [complexPolynomialInFirstMv, finOneSumToFinTwo, + MvPolynomial.monomial_eq] + +lemma rename_rightComplementMonomial_finOne_complex (d : ℕ) + (m : Fin 1 →₀ ℕ) : + MvPolynomial.rename finOneSumToFinTwo + (MvPolynomial.rightComplementMonomial + (R := ℂ) (τ := Fin 1) (fun _ : Fin 1 => d) m) = + MvPolynomial.X (1 : Fin 2) ^ (d - m 0) := by + simp [MvPolynomial.rightComplementMonomial, finOneSumToFinTwo] + +lemma complexUnivariateDegreeBoxOperator_basis (d : ℕ) + (T : ℂ[X] →ₗ[ℂ] ℂ[X]) + (m : {m : Fin 1 →₀ ℕ // ∀ i, m i ≤ d}) : + complexUnivariateDegreeBoxOperator d T + (MvPolynomial.basisDegreeOfLE (R := ℂ) (fun _ : Fin 1 => d) m) = + (MvPolynomial.uniqueAlgEquiv ℂ (Fin 1)).symm + (T (Polynomial.X ^ m.1 0)) := by + change (MvPolynomial.uniqueAlgEquiv ℂ (Fin 1)).symm + (T (MvPolynomial.uniqueAlgEquiv ℂ (Fin 1) + ((MvPolynomial.basisDegreeOfLE (R := ℂ) (fun _ : Fin 1 => d) m : + MvPolynomial.degreeOfLE (Fin 1) ℂ (fun _ => d)) : + MvPolynomial (Fin 1) ℂ))) = _ + rw [MvPolynomial.coe_basisDegreeOfLE, + MvPolynomial.uniqueAlgEquiv_monomial] + simp [Polynomial.X_pow_eq_monomial] + +/-- The genuine algebraic symbol of a complex univariate degree-box operator +is its usual finite algebraic symbol after identifying the two singleton +variable blocks with `Fin 2`. -/ +theorem rename_algebraicSymbol_complexUnivariateDegreeBoxOperator + (d : ℕ) (T : ℂ[X] →ₗ[ℂ] ℂ[X]) : + MvPolynomial.rename finOneSumToFinTwo + (MvPolynomial.algebraicSymbol (fun _ : Fin 1 => d) + (complexUnivariateDegreeBoxOperator d T)) = + complexFiniteAlgebraicSymbol d T := by + classical + rw [MvPolynomial.algebraicSymbol, map_sum] + let g : ℕ → MvPolynomial (Fin 2) ℂ := fun k => + MvPolynomial.C (Nat.choose d k : ℂ) * + complexPolynomialInFirstMv (T (Polynomial.X ^ k)) * + MvPolynomial.X 1 ^ (d - k) + calc + ∑ m : {m : Fin 1 →₀ ℕ // ∀ i, m i ≤ d}, + MvPolynomial.rename finOneSumToFinTwo + (MvPolynomial.C + (MvPolynomial.boxChoose (fun _ : Fin 1 => d) m.1 : ℂ) * + MvPolynomial.rename (Sum.inl : Fin 1 → Fin 1 ⊕ Fin 1) + (complexUnivariateDegreeBoxOperator d T + (MvPolynomial.basisDegreeOfLE + (R := ℂ) (fun _ : Fin 1 => d) m)) * + MvPolynomial.rightComplementMonomial + (R := ℂ) (τ := Fin 1) (fun _ : Fin 1 => d) m.1) = + ∑ m : {m : Fin 1 →₀ ℕ // ∀ i, m i ≤ d}, g (m.1 0) := by + apply Fintype.sum_congr + intro m + simp only [map_mul, MvPolynomial.rename_C] + rw [complexUnivariateDegreeBoxOperator_basis, + rename_uniqueAlgEquiv_symm_eq_complexPolynomialInFirstMv, + rename_rightComplementMonomial_finOne_complex] + simp [g, MvPolynomial.boxChoose, + MvPolynomial.degreeOfLEFinOneEquiv_val] + _ = ∑ k : Fin (d + 1), g k := by + apply Fintype.sum_equiv (MvPolynomial.degreeOfLEFinOneEquiv d) + intro m + simp [g, MvPolynomial.degreeOfLEFinOneEquiv_val] + _ = complexFiniteAlgebraicSymbol d T := by + simpa [g, complexFiniteAlgebraicSymbol] using + Fin.sum_univ_eq_sum_range g (d + 1) + +/-- The complex finite symbol of the complexified bidiagonal operator is the +coefficientwise complexification of the already computed real affine symbol. -/ +theorem complexFiniteAlgebraicSymbol_complexBidiagonalLinearMap + (alpha beta : ℕ → ℝ) (d : ℕ) : + complexFiniteAlgebraicSymbol d (complexBidiagonalLinearMap alpha beta) = + complexifyMv + (Challenges.BorceaBranden.finiteAlgebraicSymbol d + (bidiagonalLinearMap alpha beta)) := by + classical + rw [finiteAlgebraicSymbol_bidiagonalLinearMap] + simp only [complexFiniteAlgebraicSymbol, affineBidiagonalSymbol, + complexifyMv, map_sum] + apply Finset.sum_congr rfl + intro k hk + congr 1 + simp [complexPolynomialInFirstMv, complexBidiagonalLinearMap, + Polynomial.X_pow_eq_monomial, diagonalOperator_monomial, pow_succ] + ring + +/-- Identify variables `0` and `1` with the left and right singleton blocks. -/ +def finTwoToFinOneSum : Fin 2 → Fin 1 ⊕ Fin 1 := + Fin.cases (Sum.inl 0) (fun _ => Sum.inr 0) + +theorem finTwoToFinOneSum_comp_finOneSumToFinTwo : + finTwoToFinOneSum ∘ finOneSumToFinTwo = id := by + funext i + rcases i with i | i + · rw [Subsingleton.elim i 0] + rfl + · rw [Subsingleton.elim i 0] + rfl + +theorem finOneSumToFinTwo_comp_finTwoToFinOneSum : + finOneSumToFinTwo ∘ finTwoToFinOneSum = id := by + funext i + apply Fin.cases + · rfl + · intro j + rw [Subsingleton.elim j 0] + rfl + +/-- Borcea--Branden, Theorem 1.1, symbol identification for the complexified +bidiagonal operator. The equality uses the affine, not homogeneous, finite +symbol computed by `finiteAlgebraicSymbol_bidiagonalLinearMap`. -/ +theorem algebraicSymbol_complexBidiagonalDegreeBoxOperator + (alpha beta : ℕ → ℝ) (d : ℕ) : + MvPolynomial.algebraicSymbol (fun _ : Fin 1 => d) + (complexUnivariateDegreeBoxOperator d + (complexBidiagonalLinearMap alpha beta)) = + MvPolynomial.rename finTwoToFinOneSum + (complexifyMv + (Challenges.BorceaBranden.finiteAlgebraicSymbol d + (bidiagonalLinearMap alpha beta))) := by + have h := congrArg (MvPolynomial.rename finTwoToFinOneSum) + (rename_algebraicSymbol_complexUnivariateDegreeBoxOperator d + (complexBidiagonalLinearMap alpha beta)) + rw [complexFiniteAlgebraicSymbol_complexBidiagonalLinearMap] at h + simpa [MvPolynomial.rename_rename, + finTwoToFinOneSum_comp_finOneSumToFinTwo] using h + +/-- Explicit bidiagonal application of finite degree-box symbol sufficiency. + +This is exactly the sufficiency implication in Borcea--Branden, Theorem 1.1, +after equations (2.1)--(2.2). The symbol hypothesis is genuine bivariate +upper-half-plane stability; no Jensen-pencil or PF conclusion is assumed. -/ +theorem complexBidiagonalDegreeBox_preserves_stability + (alpha beta : ℕ → ℝ) (d : ℕ) + (hSymbol : MvUpperHalfPlaneStable + (complexifyMv + (Challenges.BorceaBranden.finiteAlgebraicSymbol d + (bidiagonalLinearMap alpha beta)))) + (f : MvPolynomial.degreeOfLE (Fin 1) ℂ (fun _ => d)) + (hf : MvUpperHalfPlaneStable f.1) : + MvUpperHalfPlaneStableOrZero + (complexUnivariateDegreeBoxOperator d + (complexBidiagonalLinearMap alpha beta) f) := by + apply finiteSymbol_finOne_preserves_stability d _ ?_ f hf + rw [algebraicSymbol_complexBidiagonalDegreeBoxOperator] + exact hSymbol.rename + end RealRooted.BorceaBranden From a7c7016607d9391dd68f7ad9987ede6e98d75d1c Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Tue, 4 Aug 2026 00:31:50 +0000 Subject: [PATCH 80/81] Deduplicate bidiagonal symbol variable equivalence --- .../Applications/BidiagonalSymbol.lean | 44 ++++++++----------- 1 file changed, 19 insertions(+), 25 deletions(-) diff --git a/RealRooted/BorceaBranden/Applications/BidiagonalSymbol.lean b/RealRooted/BorceaBranden/Applications/BidiagonalSymbol.lean index cdd041fc5..dd7a49fd5 100644 --- a/RealRooted/BorceaBranden/Applications/BidiagonalSymbol.lean +++ b/RealRooted/BorceaBranden/Applications/BidiagonalSymbol.lean @@ -192,27 +192,22 @@ theorem complexFiniteAlgebraicSymbol_complexBidiagonalLinearMap Polynomial.X_pow_eq_monomial, diagonalOperator_monomial, pow_succ] ring -/-- Identify variables `0` and `1` with the left and right singleton blocks. -/ -def finTwoToFinOneSum : Fin 2 → Fin 1 ⊕ Fin 1 := - Fin.cases (Sum.inl 0) (fun _ => Sum.inr 0) - -theorem finTwoToFinOneSum_comp_finOneSumToFinTwo : - finTwoToFinOneSum ∘ finOneSumToFinTwo = id := by - funext i - rcases i with i | i - · rw [Subsingleton.elim i 0] - rfl - · rw [Subsingleton.elim i 0] - rfl - -theorem finOneSumToFinTwo_comp_finTwoToFinOneSum : - finOneSumToFinTwo ∘ finTwoToFinOneSum = id := by - funext i - apply Fin.cases - · rfl - · intro j - rw [Subsingleton.elim j 0] - rfl +/-- Identify the left and right singleton blocks with variables `0` and `1`. -/ +def finOneSumEquivFinTwo : Fin 1 ⊕ Fin 1 ≃ Fin 2 where + toFun := finOneSumToFinTwo + invFun := Fin.cases (Sum.inl 0) (fun _ => Sum.inr 0) + left_inv i := by + rcases i with i | i + · rw [Subsingleton.elim i 0] + rfl + · rw [Subsingleton.elim i 0] + rfl + right_inv i := by + apply Fin.cases + · rfl + · intro j + rw [Subsingleton.elim j 0] + rfl /-- Borcea--Branden, Theorem 1.1, symbol identification for the complexified bidiagonal operator. The equality uses the affine, not homogeneous, finite @@ -222,16 +217,15 @@ theorem algebraicSymbol_complexBidiagonalDegreeBoxOperator MvPolynomial.algebraicSymbol (fun _ : Fin 1 => d) (complexUnivariateDegreeBoxOperator d (complexBidiagonalLinearMap alpha beta)) = - MvPolynomial.rename finTwoToFinOneSum + MvPolynomial.rename finOneSumEquivFinTwo.symm (complexifyMv (Challenges.BorceaBranden.finiteAlgebraicSymbol d (bidiagonalLinearMap alpha beta))) := by - have h := congrArg (MvPolynomial.rename finTwoToFinOneSum) + have h := congrArg (MvPolynomial.rename finOneSumEquivFinTwo.symm) (rename_algebraicSymbol_complexUnivariateDegreeBoxOperator d (complexBidiagonalLinearMap alpha beta)) rw [complexFiniteAlgebraicSymbol_complexBidiagonalLinearMap] at h - simpa [MvPolynomial.rename_rename, - finTwoToFinOneSum_comp_finOneSumToFinTwo] using h + simpa [MvPolynomial.rename_rename, finOneSumEquivFinTwo] using h /-- Explicit bidiagonal application of finite degree-box symbol sufficiency. From c35a982ec76873d2e58a744eb15c86a56706baab Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Tue, 4 Aug 2026 05:00:47 +0000 Subject: [PATCH 81/81] Repair degree-box finite-symbol applications --- .../Applications/BidiagonalSymbol.lean | 70 ++++++++++---- .../Applications/DegreeBoxPolarization.lean | 96 +++++++++---------- 2 files changed, 99 insertions(+), 67 deletions(-) diff --git a/RealRooted/BorceaBranden/Applications/BidiagonalSymbol.lean b/RealRooted/BorceaBranden/Applications/BidiagonalSymbol.lean index dd7a49fd5..31d5c5f39 100644 --- a/RealRooted/BorceaBranden/Applications/BidiagonalSymbol.lean +++ b/RealRooted/BorceaBranden/Applications/BidiagonalSymbol.lean @@ -49,18 +49,53 @@ theorem finiteAlgebraicSymbol_bidiagonalLinearMap (alpha beta : ℕ → ℝ) (d /-! ## Complex degree-box application -/ +/-- Coefficientwise complex diagonal operator. -/ +def complexDiagonalOperator (gamma : ℕ → ℂ) (p : ℂ[X]) : ℂ[X] := + p.sum fun n a => Polynomial.monomial n (gamma n * a) + +@[simp] theorem coeff_complexDiagonalOperator + (gamma : ℕ → ℂ) (p : ℂ[X]) (n : ℕ) : + (complexDiagonalOperator gamma p).coeff n = gamma n * p.coeff n := by + classical + rw [complexDiagonalOperator, Polynomial.coeff_sum] + simp only [Polynomial.coeff_monomial] + rw [Polynomial.sum_def] + simp_all + +theorem complexDiagonalOperator_add (gamma : ℕ → ℂ) (p q : ℂ[X]) : + complexDiagonalOperator gamma (p + q) = + complexDiagonalOperator gamma p + complexDiagonalOperator gamma q := by + ext n + simp [mul_add] + +theorem complexDiagonalOperator_C_mul + (gamma : ℕ → ℂ) (a : ℂ) (p : ℂ[X]) : + complexDiagonalOperator gamma (C a * p) = + C a * complexDiagonalOperator gamma p := by + ext n + simp [mul_comm, mul_left_comm] + +theorem complexDiagonalOperator_monomial + (gamma : ℕ → ℂ) (n : ℕ) (a : ℂ) : + complexDiagonalOperator gamma (Polynomial.monomial n a) = + Polynomial.monomial n (gamma n * a) := by + ext k + by_cases hk : k = n + · simp_all + · simp [Polynomial.coeff_monomial, Ne.symm hk] + /-- Complex-linear extension of the real bidiagonal operator. -/ def complexBidiagonalLinearMap (alpha beta : ℕ → ℝ) : Polynomial ℂ →ₗ[ℂ] Polynomial ℂ where toFun := fun p => - diagonalOperator (fun k => (alpha k : ℂ)) p + - Polynomial.X * diagonalOperator (fun k => (beta k : ℂ)) p + complexDiagonalOperator (fun k => (alpha k : ℂ)) p + + Polynomial.X * complexDiagonalOperator (fun k => (beta k : ℂ)) p map_add' p q := by - simp only [diagonalOperator_add, mul_add] + simp only [complexDiagonalOperator_add, mul_add] abel map_smul' c p := by - simp only [smul_eq_C_mul, diagonalOperator_C_mul] - simp [mul_comm] + simp only [smul_eq_C_mul, complexDiagonalOperator_C_mul] + simp only [RingHom.id_apply] ring /-- Regard a complex univariate polynomial as a bivariate polynomial in the @@ -163,12 +198,11 @@ theorem rename_algebraicSymbol_complexUnivariateDegreeBoxOperator rw [complexUnivariateDegreeBoxOperator_basis, rename_uniqueAlgEquiv_symm_eq_complexPolynomialInFirstMv, rename_rightComplementMonomial_finOne_complex] - simp [g, MvPolynomial.boxChoose, - MvPolynomial.degreeOfLEFinOneEquiv_val] + simp [g, MvPolynomial.boxChoose] _ = ∑ k : Fin (d + 1), g k := by - apply Fintype.sum_equiv (MvPolynomial.degreeOfLEFinOneEquiv d) + apply Fintype.sum_equiv (degreeOfLEFinOneEquiv d) intro m - simp [g, MvPolynomial.degreeOfLEFinOneEquiv_val] + simp [g, degreeOfLEFinOneEquiv_val] _ = complexFiniteAlgebraicSymbol d T := by simpa [g, complexFiniteAlgebraicSymbol] using Fin.sum_univ_eq_sum_range g (d + 1) @@ -186,11 +220,9 @@ theorem complexFiniteAlgebraicSymbol_complexBidiagonalLinearMap simp only [complexFiniteAlgebraicSymbol, affineBidiagonalSymbol, complexifyMv, map_sum] apply Finset.sum_congr rfl - intro k hk - congr 1 + intro k _ simp [complexPolynomialInFirstMv, complexBidiagonalLinearMap, - Polynomial.X_pow_eq_monomial, diagonalOperator_monomial, pow_succ] - ring + Polynomial.X_pow_eq_monomial, complexDiagonalOperator_monomial, pow_succ] /-- Identify the left and right singleton blocks with variables `0` and `1`. -/ def finOneSumEquivFinTwo : Fin 1 ⊕ Fin 1 ≃ Fin 2 where @@ -203,11 +235,7 @@ def finOneSumEquivFinTwo : Fin 1 ⊕ Fin 1 ≃ Fin 2 where · rw [Subsingleton.elim i 0] rfl right_inv i := by - apply Fin.cases - · rfl - · intro j - rw [Subsingleton.elim j 0] - rfl + fin_cases i <;> rfl /-- Borcea--Branden, Theorem 1.1, symbol identification for the complexified bidiagonal operator. The equality uses the affine, not homogeneous, finite @@ -225,7 +253,11 @@ theorem algebraicSymbol_complexBidiagonalDegreeBoxOperator (rename_algebraicSymbol_complexUnivariateDegreeBoxOperator d (complexBidiagonalLinearMap alpha beta)) rw [complexFiniteAlgebraicSymbol_complexBidiagonalLinearMap] at h - simpa [MvPolynomial.rename_rename, finOneSumEquivFinTwo] using h + have hcomp : finOneSumEquivFinTwo.symm ∘ finOneSumToFinTwo = id := by + funext i + exact finOneSumEquivFinTwo.symm_apply_apply i + rw [MvPolynomial.rename_rename, hcomp, MvPolynomial.rename_id] at h + exact h /-- Explicit bidiagonal application of finite degree-box symbol sufficiency. diff --git a/RealRooted/BorceaBranden/Applications/DegreeBoxPolarization.lean b/RealRooted/BorceaBranden/Applications/DegreeBoxPolarization.lean index 5d3b2fb21..14ff04e65 100644 --- a/RealRooted/BorceaBranden/Applications/DegreeBoxPolarization.lean +++ b/RealRooted/BorceaBranden/Applications/DegreeBoxPolarization.lean @@ -100,53 +100,6 @@ theorem sum_degreeOneExponent_degreeFunction end -/-- Finite-symbol sufficiency for a one-variable source degree box. - -This is the source-side specialization of Borcea--Branden, proof of Theorem 1.1, -using equations (2.1)--(2.2), Proposition 2.4, and Lemma 2.5 (Section 2.2, -pp. 10--12). The conclusion is zero-aware because Lemma 2.2 permits the -operator value to vanish. -/ -theorem finiteSymbol_finOne_preserves_stability - {tau : Type*} (n : ℕ) - (T : MvPolynomial.degreeOfLE (Fin 1) ℂ (fun _ => n) →ₗ[ℂ] - MvPolynomial tau ℂ) - (hSymbol : MvUpperHalfPlaneStable - (MvPolynomial.algebraicSymbol (fun _ : Fin 1 => n) T)) - (f : MvPolynomial.degreeOfLE (Fin 1) ℂ (fun _ => n)) - (hf : MvUpperHalfPlaneStable f.1) : - MvUpperHalfPlaneStableOrZero (T f) := by - have hdegree : - (MvPolynomial.uniqueAlgEquiv ℂ (Fin 1) f.1).natDegree ≤ n := by - calc - (MvPolynomial.uniqueAlgEquiv ℂ (Fin 1) f.1).natDegree = - f.1.degreeOf default := by - simpa only [AlgEquiv.symm_apply_apply] using - (MvPolynomial.degreeOf_uniqueAlgEquiv_symm (σ := Fin 1) - (MvPolynomial.uniqueAlgEquiv ℂ (Fin 1) f.1)).symm - _ ≤ n := - (MvPolynomial.mem_degreeOfLE_iff_degreeOf f.1).mp f.2 default - have hunivariate : - ∀ w : ℂ, 0 < w.im → - (MvPolynomial.uniqueAlgEquiv ℂ (Fin 1) f.1).eval w ≠ 0 := by - intro w hw - change Polynomial.eval₂ (RingHom.id ℂ) w - (MvPolynomial.uniqueAlgEquiv ℂ (Fin 1) f.1) ≠ 0 - rw [MvPolynomial.eval₂_const_uniqueAlgEquiv] - exact hf (fun _ => w) (fun _ => hw) - have hpolarized : MvUpperHalfPlaneStable - (polarizationDegreeBoxLinearMap n f).1 := by - change MvUpperHalfPlaneStable - (polarization n (MvPolynomial.uniqueAlgEquiv ℂ (Fin 1) f.1)) - exact mvUpperHalfPlaneStable_polarization hdegree hunivariate - have hlifted := finiteSymbol_preserves_stability - (sourcePolarizedOperator n T) - (mvUpperHalfPlaneStable_algebraicSymbol_sourcePolarizedOperator - n T hSymbol) - (polarizationDegreeBoxLinearMap n f) hpolarized - simpa only [sourcePolarizedOperator, LinearMap.comp_apply, - diagonalProjectionDegreeBox_comp_polarizationDegreeBoxLinearMap] using - hlifted - end RealRooted.BorceaBranden namespace MvPolynomial @@ -453,7 +406,7 @@ namespace RealRooted.BorceaBranden noncomputable section -open MvPolynomial +open _root_.MvPolynomial /-- The source-degree coefficient of a one-variable finite algebraic symbol. @@ -648,6 +601,53 @@ theorem mvUpperHalfPlaneStable_algebraicSymbol_sourcePolarizedOperator (fun _ : Fin 1 => n) T default) hstable +/-- Finite-symbol sufficiency for a one-variable source degree box. + +This is the source-side specialization of Borcea--Branden, proof of Theorem 1.1, +using equations (2.1)--(2.2), Proposition 2.4, and Lemma 2.5 (Section 2.2, +pp. 10--12). The conclusion is zero-aware because Lemma 2.2 permits the +operator value to vanish. -/ +theorem finiteSymbol_finOne_preserves_stability + {tau : Type*} (n : ℕ) + (T : degreeOfLE (Fin 1) ℂ (fun _ => n) →ₗ[ℂ] + MvPolynomial tau ℂ) + (hSymbol : MvUpperHalfPlaneStable + (algebraicSymbol (fun _ : Fin 1 => n) T)) + (f : degreeOfLE (Fin 1) ℂ (fun _ => n)) + (hf : MvUpperHalfPlaneStable f.1) : + MvUpperHalfPlaneStableOrZero (T f) := by + have hdegree : + (uniqueAlgEquiv ℂ (Fin 1) f.1).natDegree ≤ n := by + calc + (uniqueAlgEquiv ℂ (Fin 1) f.1).natDegree = + f.1.degreeOf default := by + simpa only [AlgEquiv.symm_apply_apply] using + (degreeOf_uniqueAlgEquiv_symm (σ := Fin 1) + (uniqueAlgEquiv ℂ (Fin 1) f.1)).symm + _ ≤ n := + (mem_degreeOfLE_iff_degreeOf f.1).mp f.2 default + have hunivariate : + ∀ w : ℂ, 0 < w.im → + (uniqueAlgEquiv ℂ (Fin 1) f.1).eval w ≠ 0 := by + intro w hw + change Polynomial.eval₂ (RingHom.id ℂ) w + (uniqueAlgEquiv ℂ (Fin 1) f.1) ≠ 0 + rw [eval₂_const_uniqueAlgEquiv] + exact hf (fun _ => w) (fun _ => hw) + have hpolarized : MvUpperHalfPlaneStable + (polarizationDegreeBoxLinearMap n f).1 := by + change MvUpperHalfPlaneStable + (polarization n (uniqueAlgEquiv ℂ (Fin 1) f.1)) + exact mvUpperHalfPlaneStable_polarization hdegree hunivariate + have hlifted := finiteSymbol_preserves_stability + (sourcePolarizedOperator n T) + (mvUpperHalfPlaneStable_algebraicSymbol_sourcePolarizedOperator + n T hSymbol) + (polarizationDegreeBoxLinearMap n f) hpolarized + simpa only [sourcePolarizedOperator, LinearMap.comp_apply, + diagonalProjectionDegreeBox_comp_polarizationDegreeBoxLinearMap] using + hlifted + /-- Termwise form of the source-polarized algebraic symbol after identifying all polarized source variables. -/ theorem rename_algebraicSymbol_sourcePolarizedOperator_eq_sum