From b844f45f2546d22b86ca326ef026e7740c7a0736 Mon Sep 17 00:00:00 2001
From: Per Alexandersson <per.w.alexandersson@gmail.com>
Date: Mon, 3 Aug 2026 23:17:33 +0000
Subject: [PATCH 1/2] Bundle zero-aware real-rooted interlacing sequences

---
 RealRooted/InterlacingSequenceBasic.lean | 62 ++++++++++++++++++++++++
 RealRooted/ProductFamily.lean            |  7 ++-
 2 files changed, 65 insertions(+), 4 deletions(-)

diff --git a/RealRooted/InterlacingSequenceBasic.lean b/RealRooted/InterlacingSequenceBasic.lean
index cf83eeae..60f92d75 100644
--- a/RealRooted/InterlacingSequenceBasic.lean
+++ b/RealRooted/InterlacingSequenceBasic.lean
@@ -255,4 +255,66 @@ lemma IsInterlacingSeq0Nonneg.filter_ne_zero_of_realRooted
       of_decide_eq_true (List.mem_filter.mp hgj_mem).2
     exact hfg0.toPrec_of_ne hfi_ne hgj_ne
 
+/-! ## Zero-aware sequences with elementwise real-rootedness -/
+
+/-- A weak zero-aware nonnegative interlacing sequence together with the
+real-rootedness of every nonzero member. This bundles a side condition used
+throughout the matrix and product-family APIs without strengthening
+`IsInterlacingSeq0Nonneg`. -/
+def IsInterlacingSeq0NonnegRealRooted (fs : List ℝ[X]) : Prop :=
+  IsInterlacingSeq0Nonneg fs ∧
+    ∀ f ∈ fs, f ≠ 0 → (f ≠ 0 ∧ f.Splits)
+
+namespace IsInterlacingSeq0NonnegRealRooted
+
+lemma interlacingSeq0Nonneg {fs : List ℝ[X]}
+    (hfs : IsInterlacingSeq0NonnegRealRooted fs) :
+    IsInterlacingSeq0Nonneg fs :=
+  hfs.1
+
+lemma interlacingSeq0 {fs : List ℝ[X]}
+    (hfs : IsInterlacingSeq0NonnegRealRooted fs) :
+    IsInterlacingSeq0 fs :=
+  hfs.1.1
+
+lemma nonnegCoeffs {fs : List ℝ[X]}
+    (hfs : IsInterlacingSeq0NonnegRealRooted fs) :
+    ∀ f ∈ fs, HasNonnegCoeffs f :=
+  hfs.1.2
+
+lemma realRooted {fs : List ℝ[X]}
+    (hfs : IsInterlacingSeq0NonnegRealRooted fs) :
+    ∀ f ∈ fs, f ≠ 0 → (f ≠ 0 ∧ f.Splits) :=
+  hfs.2
+
+lemma splits {fs : List ℝ[X]}
+    (hfs : IsInterlacingSeq0NonnegRealRooted fs) {f : ℝ[X]}
+    (hf : f ∈ fs) (hf_ne : f ≠ 0) :
+    f.Splits :=
+  (hfs.2 f hf hf_ne).2
+
+lemma sublist {fs gs : List ℝ[X]}
+    (hfs : IsInterlacingSeq0NonnegRealRooted fs) (hgs : gs.Sublist fs) :
+    IsInterlacingSeq0NonnegRealRooted gs :=
+  ⟨⟨hfs.1.1.sublist hgs, fun f hf ⇒ hfs.1.2 f (hgs.subset hf)⟩,
+    fun f hf ⇒ hfs.2 f (hgs.subset hf)⟩
+
+lemma sublist_of_ne {fs gs : List ℝ[X]}
+    (hfs : IsInterlacingSeq0NonnegRealRooted fs) (hgs : gs.Sublist fs)
+    (hne : ∀ f ∈ gs, f ≠ 0) :
+    IsInterlacingSeqNonneg gs :=
+  hfs.1.sublist_of_realRooted_of_ne hgs hfs.2 hne
+
+lemma filter_ne_zero {fs : List ℝ[X]}
+    (hfs : IsInterlacingSeq0NonnegRealRooted fs) :
+    IsInterlacingSeqNonneg (fs.filter (· ≠ 0)) :=
+  hfs.1.filter_ne_zero_of_realRooted hfs.2
+
+end IsInterlacingSeq0NonnegRealRooted
+
+lemma IsInterlacingSeqNonneg.toIsInterlacingSeq0NonnegRealRooted
+    {fs : List ℝ[X]} (hfs : IsInterlacingSeqNonneg fs) :
+    IsInterlacingSeq0NonnegRealRooted fs :=
+  ⟨hfs.toIsInterlacingSeq0Nonneg, fun f hf _ ⇒ hfs.realRooted f hf⟩
+
 end RealRooted
diff --git a/RealRooted/ProductFamily.lean b/RealRooted/ProductFamily.lean
index 73066749..a2a68ba2 100644
--- a/RealRooted/ProductFamily.lean
+++ b/RealRooted/ProductFamily.lean
@@ -464,11 +464,10 @@ lemma mem_filterProductRightNonzero_ne_zero {fs gs : List ℝ[X]} {g : ℝ[X]}
 
 private lemma interlacingSeqNonneg_filterLeftNonzero
     {fs gs : List ℝ[X]} (hlen : fs.length = gs.length)
-    (hfs : IsInterlacingSeq0Nonneg fs)
-    (hfs_real : ∀ f ∈ fs, f ≠ 0 → (f ≠ 0 ∧ f.Splits)) :
+    (hfs : IsInterlacingSeq0NonnegRealRooted fs) :
     IsInterlacingSeqNonneg (filterLeftNonzero fs gs) := by
   rw [filterLeftNonzero_eq_filter_ne_zero hlen]
-  exact IsInterlacingSeq0Nonneg.filter_ne_zero_of_realRooted hfs hfs_real
+  exact hfs.filter_ne_zero
 
 private lemma interlacingSeqNonneg_filterProductLeftNonzero
     {fs gs : List ℝ[X]} (hfs : IsInterlacingSeq0Nonneg fs)
@@ -544,7 +543,7 @@ theorem isRealRooted_zipWith_mul_sum_reverse_of_interlacingSeq0Nonneg
   have hfs' : IsInterlacingSeqNonneg fs' := by
     simpa [fs'] using interlacingSeqNonneg_filterLeftNonzero
       (fs := fs) (gs := gs.reverse) (by simp_all)
-      hfs hfs_real
+      ⟨hfs, hfs_real⟩
   have hgs'_rev : IsInterlacingSeqNonneg gs'.reverse := by
     exact interlacingSeqNonneg_reverse_of_sublist_reverse hgs <| by
       simpa [gs'] using filterRightByLeftNonzero_sublist_right fs gs.reverse

From b2c126d773bdec7191ac8c0cc6880ed7973b7a34 Mon Sep 17 00:00:00 2001
From: Per Alexandersson <per.w.alexandersson@gmail.com>
Date: Mon, 3 Aug 2026 23:27:06 +0000
Subject: [PATCH 2/2] Fix interlacing bundle lambda syntax

---
 RealRooted/InterlacingSequenceBasic.lean | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/RealRooted/InterlacingSequenceBasic.lean b/RealRooted/InterlacingSequenceBasic.lean
index 60f92d75..0ff0a09c 100644
--- a/RealRooted/InterlacingSequenceBasic.lean
+++ b/RealRooted/InterlacingSequenceBasic.lean
@@ -296,8 +296,8 @@ lemma splits {fs : List ℝ[X]}
 lemma sublist {fs gs : List ℝ[X]}
     (hfs : IsInterlacingSeq0NonnegRealRooted fs) (hgs : gs.Sublist fs) :
     IsInterlacingSeq0NonnegRealRooted gs :=
-  ⟨⟨hfs.1.1.sublist hgs, fun f hf ⇒ hfs.1.2 f (hgs.subset hf)⟩,
-    fun f hf ⇒ hfs.2 f (hgs.subset hf)⟩
+  ⟨⟨hfs.1.1.sublist hgs, fun f hf => hfs.1.2 f (hgs.subset hf)⟩,
+    fun f hf => hfs.2 f (hgs.subset hf)⟩
 
 lemma sublist_of_ne {fs gs : List ℝ[X]}
     (hfs : IsInterlacingSeq0NonnegRealRooted fs) (hgs : gs.Sublist fs)
@@ -315,6 +315,6 @@ end IsInterlacingSeq0NonnegRealRooted
 lemma IsInterlacingSeqNonneg.toIsInterlacingSeq0NonnegRealRooted
     {fs : List ℝ[X]} (hfs : IsInterlacingSeqNonneg fs) :
     IsInterlacingSeq0NonnegRealRooted fs :=
-  ⟨hfs.toIsInterlacingSeq0Nonneg, fun f hf _ ⇒ hfs.realRooted f hf⟩
+  ⟨hfs.toIsInterlacingSeq0Nonneg, fun f hf _ => hfs.realRooted f hf⟩
 
 end RealRooted