Document Hoster-Stump lower-sum obstruction

RealRooted.lean

@@ -131,6 +131,7 @@ import RealRooted.Hadamard
 import RealRooted.HadamardProduct
 import RealRooted.HeilmannLieb
 import RealRooted.HermiteBiehler
+import RealRooted.HosterStumpInterlacing
 import RealRooted.HurwitzMatrix
 import RealRooted.InterlacingSequence
 import RealRooted.InterlacingSequenceBasic

RealRooted/Basic.lean

@@ -557,6 +557,207 @@ def Prec (f g : ℝ[X]) : Prop := (f ≠ 0 ∧ f.Splits) ∧ (g ≠ 0 ∧ g.Spli
     ((ss.length + 1 = rs.length ∧ ListInterlaces ss rs) ∨
       (ss.length = rs.length ∧ ListAlternates ss rs))
 
+private lemma listInterlaces_right_tail_ge :
+    ∀ {ss rs : List ℝ} {r : ℝ}, ListInterlaces ss (r :: rs) → ∀ x ∈ rs, r ≤ x
+  | [], [], _, _ => by simp
+  | [], _ :: _, _, h => by simp [ListInterlaces] at h
+  | _ :: _, [], _, _ => by simp
+  | s :: ss, r₂ :: rs, r, h => by
+      rcases h with ⟨hr_s, hs_r₂, htail⟩
+      intro x hx
+      rcases List.mem_cons.mp hx with rfl | hx
+      · exact le_trans hr_s hs_r₂
+      · exact le_trans (le_trans hr_s hs_r₂)
+          (listInterlaces_right_tail_ge htail x hx)
+
+private lemma listInterlaces_left_ge_head :
+    ∀ {ss rs : List ℝ} {r : ℝ}, ListInterlaces ss (r :: rs) → ∀ x ∈ ss, r ≤ x
+  | [], _, _, _ => by simp
+  | _ :: _, [], _, h => by simp [ListInterlaces] at h
+  | s :: ss, r₂ :: rs, r, h => by
+      rcases h with ⟨hr_s, hs_r₂, htail⟩
+      intro x hx
+      rcases List.mem_cons.mp hx with rfl | hx
+      · exact hr_s
+      · exact le_trans (le_trans hr_s hs_r₂)
+          (listInterlaces_left_ge_head htail x hx)
+
+private lemma listInterlaces_count_left_le_right_of_head (u : ℝ) :
+    ∀ {ss rs : List ℝ}, ListInterlaces ss (u :: rs) →
+      ss.count u ≤ (u :: rs).count u
+  | [], _, _ => by simp
+  | _ :: _, [], h => by simp [ListInterlaces] at h
+  | s :: ss, r₂ :: rs, h => by
+      rcases h with ⟨hus, hs_r₂, htail⟩
+      by_cases hs : s = u
+      · subst s
+        by_cases hr₂ : r₂ = u
+        · subst r₂
+          have ih := listInterlaces_count_left_le_right_of_head u htail
+          simp at ih ⊢
+          lia
+        · have hu_lt_r₂ : u < r₂ := lt_of_le_of_ne hs_r₂ (Ne.symm hr₂)
+          have htail_no_mem : u ∉ r₂ :: rs := by
+            intro hu_mem
+            rcases List.mem_cons.mp hu_mem with hu_eq | hu_rs
+            · exact hr₂ hu_eq.symm
+            · have hge := listInterlaces_right_tail_ge htail u hu_rs
+              linarith
+          have hss_no_mem : u ∉ ss := by
+            intro hu_mem
+            have hge := listInterlaces_left_ge_head htail u hu_mem
+            linarith
+          simp [List.count_eq_zero.mpr htail_no_mem,
+            List.count_eq_zero.mpr hss_no_mem]
+      · have hu_lt_s : u < s := lt_of_le_of_ne hus (Ne.symm hs)
+        have hu_lt_r₂ : u < r₂ := lt_of_lt_of_le hu_lt_s hs_r₂
+        have htail_no_mem : u ∉ r₂ :: rs := by
+          intro hu_mem
+          rcases List.mem_cons.mp hu_mem with hu_eq | hu_rs
+          · exact ne_of_gt hu_lt_r₂ hu_eq.symm
+          · have hge := listInterlaces_right_tail_ge htail u hu_rs
+            linarith
+        have hss_no_mem : u ∉ ss := by
+          intro hu_mem
+          have hge := listInterlaces_left_ge_head htail u hu_mem
+          linarith
+        simp [hs, List.count_eq_zero.mpr htail_no_mem,
+          List.count_eq_zero.mpr hss_no_mem]
+
+private lemma listInterlaces_count_right_le_left_add_one (u : ℝ) :
+    ∀ {ss rs : List ℝ}, ListInterlaces ss rs → rs.count u ≤ ss.count u + 1
+  | [], [], _ => by simp
+  | [], [r], _ => by
+      by_cases hr : r = u <;> simp [hr]
+  | [], _ :: _ :: _, h => by simp [ListInterlaces] at h
+  | _ :: _, [], h => by simp [ListInterlaces] at h
+  | _ :: _, [_], h => by simp [ListInterlaces] at h
+  | s :: ss, r₁ :: r₂ :: rs, h => by
+      rcases h with ⟨hr₁s, hs_r₂, htail⟩
+      by_cases hr₁ : r₁ = u
+      · by_cases hs : s = u
+        · subst r₁
+          subst s
+          have ih := listInterlaces_count_right_le_left_add_one u htail
+          simp [List.count_cons] at ih ⊢
+          lia
+        · subst r₁
+          have hu_lt_s : u < s := lt_of_le_of_ne hr₁s (by simpa [eq_comm] using hs)
+          have hu_lt_r₂ : u < r₂ := lt_of_lt_of_le hu_lt_s hs_r₂
+          have htail_no_mem : u ∉ r₂ :: rs := by
+            intro hu_mem
+            rcases List.mem_cons.mp hu_mem with hu_eq | hu_rs
+            · exact ne_of_gt hu_lt_r₂ hu_eq.symm
+            · have hge := listInterlaces_right_tail_ge htail u hu_rs
+              linarith
+          have htail_count : (r₂ :: rs).count u = 0 :=
+            List.count_eq_zero.mpr htail_no_mem
+          have hss_no_mem : u ∉ ss := by
+            intro hu_mem
+            have hge := listInterlaces_left_ge_head htail u hu_mem
+            linarith
+          have hss_count : ss.count u = 0 := List.count_eq_zero.mpr hss_no_mem
+          simp [htail_count, hss_count, hs]
+      · have ih := listInterlaces_count_right_le_left_add_one u htail
+        by_cases hs : s = u
+        · simp [hr₁, hs] at ih ⊢
+          lia
+        · simpa [hr₁, hs] using ih
+
+private lemma listInterlaces_count_left_le_right_add_one (u : ℝ) :
+    ∀ {ss rs : List ℝ}, ListInterlaces ss rs → ss.count u ≤ rs.count u + 1
+  | [], [], _ => by simp
+  | [], [_], _ => by simp
+  | [], _ :: _ :: _, h => by simp [ListInterlaces] at h
+  | _ :: _, [], h => by simp [ListInterlaces] at h
+  | _ :: _, [_], h => by simp [ListInterlaces] at h
+  | s :: ss, r₁ :: r₂ :: rs, h => by
+      rcases h with ⟨hr₁s, hs_r₂, htail⟩
+      have ih := listInterlaces_count_left_le_right_add_one u htail
+      by_cases hs : s = u
+      · by_cases hr₁ : r₁ = u
+        · simp [hs, hr₁] at ih ⊢
+          lia
+        · by_cases hr₂ : r₂ = u
+          · subst r₂
+            have hstrong := listInterlaces_count_left_le_right_of_head u htail
+            simp [hs, hr₁] at hstrong ⊢
+            lia
+          · have hu_lt_r₂ : u < r₂ := by
+              rw [hs] at hs_r₂
+              exact lt_of_le_of_ne hs_r₂ (Ne.symm hr₂)
+            have htail_no_mem : u ∉ r₂ :: rs := by
+              intro hu_mem
+              rcases List.mem_cons.mp hu_mem with hu_eq | hu_rs
+              · exact hr₂ hu_eq.symm
+              · have hge := listInterlaces_right_tail_ge htail u hu_rs
+                linarith
+            have hss_no_mem : u ∉ ss := by
+              intro hu_mem
+              have hge := listInterlaces_left_ge_head htail u hu_mem
+              linarith
+            have htail_count : (r₂ :: rs).count u = 0 :=
+              List.count_eq_zero.mpr htail_no_mem
+            have hss_count : ss.count u = 0 := List.count_eq_zero.mpr hss_no_mem
+            simp [hs, hr₁, htail_count, hss_count]
+      · by_cases hr₁ : r₁ = u
+        · simp [hs, hr₁] at ih ⊢
+          lia
+        · simp [hs, hr₁] at ih ⊢
+          lia
+
+private lemma listAlternates_count_bounds (u : ℝ) :
+    ∀ {ss rs : List ℝ}, ListAlternates ss rs →
+      ss.count u ≤ rs.count u + 1 ∧ rs.count u ≤ ss.count u + 1
+  | [], [], _ => by simp
+  | [], _ :: _, h => by simp [ListAlternates] at h
+  | _ :: _, [], h => by simp [ListAlternates] at h
+  | s :: ss, r :: rs, h => by
+      rcases h with ⟨hsr, htail⟩
+      constructor
+      · have ih := listInterlaces_count_left_le_right_add_one u htail
+        by_cases hs : s = u
+        · by_cases hr : r = u
+          · subst r
+            have hstrong := listInterlaces_count_left_le_right_of_head u htail
+            simp [hs] at hstrong ⊢
+            lia
+          · have hu_lt_r : u < r := by
+              rw [hs] at hsr
+              exact lt_of_le_of_ne hsr (Ne.symm hr)
+            have hss_no_mem : u ∉ ss := by
+              intro hu_mem
+              have hge := listInterlaces_left_ge_head htail u hu_mem
+              linarith
+            have hss_count : ss.count u = 0 := List.count_eq_zero.mpr hss_no_mem
+            simp [hs, hr, hss_count]
+        · simpa [hs] using ih
+      · have ih := listInterlaces_count_right_le_left_add_one u htail
+        by_cases hs : s = u
+        · simp [hs] at ih ⊢
+          lia
+        · simpa [hs] using ih
+
+/-- In proper position, the multiplicities of every real root differ by at
+most one. -/
+theorem rootMultiplicity_bounds_of_prec {f g : ℝ[X]} (h : Prec f g) (u : ℝ) :
+    f.rootMultiplicity u - 1 ≤ g.rootMultiplicity u ∧
+      g.rootMultiplicity u - 1 ≤ f.rootMultiplicity u := by
+  rcases h with ⟨_, _, ss, rs, _, _, hss_eq, hrs_eq, hshape⟩
+  have hcount : ss.count u ≤ rs.count u + 1 ∧ rs.count u ≤ ss.count u + 1 := by
+    rcases hshape with ⟨_, hint⟩ | ⟨_, halt⟩
+    · exact ⟨listInterlaces_count_left_le_right_add_one u hint,
+        listInterlaces_count_right_le_left_add_one u hint⟩
+    · exact listAlternates_count_bounds u halt
+  have hrs_count : rs.count u = g.rootMultiplicity u := by
+    rw [← count_roots g, ← hrs_eq]
+    exact (Multiset.coe_count u rs).symm
+  have hss_count : ss.count u = f.rootMultiplicity u := by
+    rw [← count_roots f, ← hss_eq]
+    exact (Multiset.coe_count u ss).symm
+  rw [hss_count, hrs_count] at hcount
+  lia
+
 lemma natDegree_bounds_of_prec {f g : ℝ[X]} (hfg : Prec f g) :
     f.natDegree ≤ g.natDegree ∧ g.natDegree ≤ f.natDegree + 1 := by
   rcases hfg with ⟨hf, hg, ss, rs, _, _, hss_eq, hrs_eq, _⟩

RealRooted/Challenges/BorceaBranden.lean

@@ -45,8 +45,14 @@ def PreservesRealRootedUpTo
     (d : ℕ) (T : ℝ[X] →ₗ[ℝ] ℝ[X]) : Prop :=
   ∀ {p : ℝ[X]}, p.natDegree ≤ d → p.Splits → T p = 0 ∨ (T p).Splits
 
-/-- Finite-degree Borcea--Branden algebraic-symbol theorem, as a named
-classical interface. -/
+/-- The positive-symbol sufficiency direction of Borcea--Branden,
+Theorem 1.2(b), specialized to one real source variable of degree at most `d`.
+
+The paper's symbol is `T((z + w)^d)`, which is `finiteAlgebraicSymbol d T`
+after expanding in the monomial basis. The complex counterpart is
+Theorem 1.1(b). The statement below records only the application-facing
+implication to real-rooted inputs and zero-aware outputs, not the converse,
+the signed-symbol branch, or the low-rank alternative. -/
 def finiteSymbolTheoremStatement : Prop :=
   ∀ {d : ℕ} {T : ℝ[X] →ₗ[ℝ] ℝ[X]},
     MvUpperHalfPlaneStable (complexifyMv (finiteAlgebraicSymbol d T)) →

RealRooted/Challenges/BraunJal.lean

@@ -101,16 +101,14 @@ abbrev OrderPolytopeHStarTheorem41Target
     (hStar : NonNestingRookPolynomialFamily) : Prop :=
   OrderPolytopeHStarTheorem41Statement hStar
 
-/-- Concrete Braun--Jal Theorem 4.1 from the accepted combinatorial model
-inputs.  The parameter-two Narayana identity is the board-model fact; all
-proper-position and real-rootedness deductions are checked in Lean. -/
+/-- Braun--Jal Theorem 4.1 from the accepted combinatorial model inputs.
+The recurrence and coefficient hypotheses are the source board-model facts;
+all proper-position and real-rootedness deductions are checked in Lean. -/
 theorem theorem41_of_modifiedModelInputs
     {M : NonNestingRookPolynomialFamily}
     (hrec2 : AuxiliaryGRecurrence ModifiedNarayanaPolynomial AuxiliaryG)
     (hH_nonneg : ∀ n : ℕ, 1 ≤ n →
       HasNonnegCoeffs (AuxiliaryG n - AuxiliaryG (n - 1)))
-    (hG_model : ∀ n : ℕ, 1 ≤ n →
-      AuxiliaryG n = C (n : ℝ) * narayanaPolynomial 2 (n - 1))
     (hrec : Theorem35GeneralizedSnakeRecurrenceStatement M
       ModifiedNarayanaPolynomial AuxiliaryG)
     (hM_nonneg : ∀ w : SnakeWord, HasNonnegCoeffs (M w))
@@ -119,8 +117,37 @@ theorem theorem41_of_modifiedModelInputs
     (hM_const : ∀ {w : SnakeWord}, w.IsConstant →
       M w = ModifiedNarayanaPolynomial (w.length + 1)) :
     Theorem41Target M :=
-  theorem41NonNestingRook_modified_of_modelInputs hrec2 hH_nonneg hG_model
-    hrec hM_nonneg hdeg hM_const
+  theorem41NonNestingRook_modified_of_sourceInputs hrec2 hH_nonneg hrec
+    hM_nonneg hdeg hM_const
+
+/-- Braun--Jal Theorem 4.1 for the concrete generalized-snake rook model.
+
+The five hypotheses are intentionally the combinatorial trust boundary from
+Braun--Jal, arXiv:2607.00922v1.  Equation `(2)` defines the auxiliary family,
+`hH_nonneg` comes from its board-difference interpretation, `hrec` is Theorem
+3.5, `hdeg` is the maximum-rook/degree identity, and `hM_const` identifies
+constant snake boards with staircases.  Formalizing the entire rook-placement
+model is outside the present scope.  All analytic conclusions are derived in
+Lean. -/
+theorem generalizedSnakeRookModel_theorem41
+    (hrec2 : AuxiliaryGRecurrence ModifiedNarayanaPolynomial AuxiliaryG)
+    (hH_nonneg : ∀ n : ℕ, 1 ≤ n →
+      HasNonnegCoeffs (AuxiliaryG n - AuxiliaryG (n - 1)))
+    (hrec : Theorem35GeneralizedSnakeRecurrenceStatement
+      generalizedSnakeRookModel.snakePolynomial
+      ModifiedNarayanaPolynomial AuxiliaryG)
+    (hdeg : ∀ {w : SnakeWord}, 1 ≤ w.length →
+      (generalizedSnakeRookModel.snakePolynomial w.deleteFinal).natDegree + 1 =
+        (generalizedSnakeRookModel.snakePolynomial w).natDegree)
+    (hM_const : ∀ {w : SnakeWord}, w.IsConstant →
+      generalizedSnakeRookModel.snakePolynomial w =
+        ModifiedNarayanaPolynomial (w.length + 1)) :
+    Theorem41Target generalizedSnakeRookModel.snakePolynomial := by
+  exact theorem41_of_modifiedModelInputs hrec2 hH_nonneg hrec
+    (fun w => by
+      rw [generalizedSnakeRookModel_snakePolynomial]
+      exact FiniteSkewBoard.rookPolynomial_hasNonnegCoeffs _)
+    hdeg hM_const
 
 /-- Order-polytope `h*` form of Braun--Jal Theorem 4.1 from the accepted
 combinatorial model inputs.  The matching hypothesis is the Stanley/
@@ -131,8 +158,6 @@ theorem orderPolytopeHStarTheorem41_of_modifiedModelInputs
     (hrec2 : AuxiliaryGRecurrence ModifiedNarayanaPolynomial AuxiliaryG)
     (hH_nonneg : ∀ n : ℕ, 1 ≤ n →
       HasNonnegCoeffs (AuxiliaryG n - AuxiliaryG (n - 1)))
-    (hG_model : ∀ n : ℕ, 1 ≤ n →
-      AuxiliaryG n = C (n : ℝ) * narayanaPolynomial 2 (n - 1))
     (hrec : Theorem35GeneralizedSnakeRecurrenceStatement M
       ModifiedNarayanaPolynomial AuxiliaryG)
     (hM_nonneg : ∀ w : SnakeWord, HasNonnegCoeffs (M w))
@@ -143,8 +168,8 @@ theorem orderPolytopeHStarTheorem41_of_modifiedModelInputs
     (hmatch : OrderPolytopeHStarMatchesNonNestingRook hStar M) :
     OrderPolytopeHStarTheorem41Target hStar :=
   orderPolytopeHStarTheorem41_of_theorem41
-    (theorem41_of_modifiedModelInputs hrec2 hH_nonneg hG_model hrec
-      hM_nonneg hdeg hM_const)
+    (theorem41_of_modifiedModelInputs hrec2 hH_nonneg hrec hM_nonneg hdeg
+      hM_const)
     hmatch
 
 /-- The real-rootedness projection of Braun--Jal Theorem 4.1. -/