diff --git a/RealRooted/Mathlib/LinearAlgebra/Matrix/SignVariation.lean b/RealRooted/Mathlib/LinearAlgebra/Matrix/SignVariation.lean
index e1c483eb..1be1cb73 100644
--- a/RealRooted/Mathlib/LinearAlgebra/Matrix/SignVariation.lean
+++ b/RealRooted/Mathlib/LinearAlgebra/Matrix/SignVariation.lean
@@ -3,6 +3,8 @@ module
 public import Mathlib.Algebra.Polynomial.RuleOfSigns
 public import Mathlib.Data.List.ChainOfFn
 public import Mathlib.Data.List.NodupEquivFin
+public import Mathlib.Data.List.SplitBy
+public import Mathlib.Order.Monotone.Extension
 public import Mathlib.Tactic
 
 /-!
@@ -29,6 +31,10 @@ lemma sign_neg_real (x : ℝ) : SignType.sign (-x) = -SignType.sign x := by
   · have hneg : -x < 0 := by linarith
     rw [sign_neg hneg, sign_pos hx]
 
+lemma eq_neg_of_ne_of_ne_zero {s t : SignType} (hs : s ≠ 0) (ht : t ≠ 0)
+    (hst : s ≠ t) : s = -t := by
+  cases s <;> cases t <;> simp_all
+
 end SignType
 
 namespace List
@@ -356,6 +362,81 @@ lemma signVariations_append_nonpos_le_succ (l₁ l₂ : List ℝ)
 
 end List
 
+namespace List
+
+private theorem exists_monotone_destutter_index {α β : Type*} [DecidableEq β]
+    (key : α → β) :
+    ∀ (l : List α), l ≠ [] →
+      ∃ block : Fin l.length → Fin ((l.map key).destutter (· ≠ ·)).length,
+        Monotone block ∧ Function.Surjective block ∧
+          ∀ i, key (l.get i) = ((l.map key).destutter (· ≠ ·)).get (block i)
+  | [], h => (h rfl).elim
+  | [a], _ => by
+      refine ⟨id, monotone_id, Function.surjective_id, ?_⟩
+      intro i
+      fin_cases i
+      rfl
+  | a :: b :: l, _ => by
+      obtain ⟨block, hmono, hsurj, hkey⟩ :=
+        exists_monotone_destutter_index key (b :: l) (by simp)
+      by_cases hab : key a = key b
+      · have hdest :
+            (((a :: b :: l).map key).destutter (· ≠ ·)) =
+              (((b :: l).map key).destutter (· ≠ ·)) := by
+          simp only [map_cons, destutter_cons_cons]
+          rw [if_neg (by simpa using hab), hab]
+          rfl
+        rw [hdest]
+        let newBlock :
+            Fin (a :: b :: l).length →
+              Fin (((b :: l).map key).destutter (· ≠ ·)).length :=
+          Fin.cases (block 0) block
+        refine ⟨newBlock, ?_, ?_, ?_⟩
+        · rw [Fin.monotone_iff_le_succ]
+          intro i
+          refine Fin.cases ?_ (fun j => ?_) i
+          · change block 0 ≤ block 0
+            exact le_rfl
+          · simpa [newBlock] using (Fin.monotone_iff_le_succ.mp hmono j)
+        · intro i
+          obtain ⟨j, rfl⟩ := hsurj i
+          exact ⟨j.succ, by simp [newBlock]⟩
+        · intro i
+          refine Fin.cases ?_ (fun j => ?_) i
+          · simpa [newBlock, hab] using hkey (0 : Fin (b :: l).length)
+          · simpa [newBlock] using hkey j
+      · have hdest :
+            (((a :: b :: l).map key).destutter (· ≠ ·)) =
+              key a :: ((b :: l).map key).destutter (· ≠ ·) := by
+          simp only [map_cons, destutter_cons_cons]
+          rw [if_pos hab]
+          rfl
+        rw [hdest]
+        let newBlock :
+            Fin (a :: b :: l).length →
+              Fin (key a :: ((b :: l).map key).destutter (· ≠ ·)).length :=
+          Fin.cases 0 fun i => (block i).succ
+        refine ⟨newBlock, ?_, ?_, ?_⟩
+        · rw [Fin.monotone_iff_le_succ]
+          intro i
+          refine Fin.cases ?_ (fun j => ?_) i
+          · change (0 : Fin (key a :: ((b :: l).map key).destutter (· ≠ ·)).length) ≤
+              (block 0).succ
+            exact bot_le
+          · change (block j.castSucc).val + 1 ≤ (block j.succ).val + 1
+            exact Nat.succ_le_succ (Fin.monotone_iff_le_succ.mp hmono j)
+        · intro i
+          refine Fin.cases ?_ (fun j => ?_) i
+          · exact ⟨0, by simp [newBlock]⟩
+          · obtain ⟨k, rfl⟩ := hsurj j
+            exact ⟨k.succ, by simp [newBlock]⟩
+        · intro i
+          refine Fin.cases ?_ (fun j => ?_) i
+          · simp [newBlock]
+          · simpa [newBlock] using hkey j
+
+end List
+
 namespace Fin
 
 /-- The number of sign changes in a finite vector, in index order and ignoring
@@ -453,6 +534,210 @@ lemma signVariations_append_nonpos_le_succ {m n : ℕ} (x : Fin m → ℝ)
     obtain ⟨i, rfl⟩ := ha
     exact hy i)
 
+/-- A decomposition of a nonzero finite real vector into consecutive sign blocks.
+
+The block count is one more than the number of sign variations. Every block has
+a nonzero coordinate, and zeros are assigned monotonically to neighboring sign
+blocks. This is the finite combinatorial decomposition used in Karlin, *Total
+Positivity*, Vol. I, Chapter V, Section 1, Theorem 1.2. -/
+structure SignBlockDecomposition {n : ℕ} (x : Fin n → ℝ) where
+  /-- The number of consecutive nonzero sign blocks. -/
+  blockCount : ℕ
+  blockCount_eq : blockCount = signVariations x + 1
+  /-- The weakly increasing block index assigned to each vector position. -/
+  block : Fin n → Fin blockCount
+  monotone_block : Monotone block
+  block_has_nonzero : ∀ b, ∃ i, block i = b ∧ x i ≠ 0
+  /-- The nonzero sign carried by each block. -/
+  blockSign : Fin blockCount → SignType
+  blockSign_ne_zero : ∀ b, blockSign b ≠ 0
+  sign_eq_blockSign : ∀ i, x i ≠ 0 → SignType.sign (x i) = blockSign (block i)
+  adjacent_blockSign :
+    ∀ {i j : Fin blockCount},
+      (i : ℕ) + 1 = (j : ℕ) → blockSign i = -blockSign j
+
+namespace SignBlockDecomposition
+
+/-- The consecutive list blocks induced by a sign-block index map. -/
+def blocks {n : ℕ} {x : Fin n → ℝ} (D : SignBlockDecomposition x) :
+    List (List (Fin n)) :=
+  (List.finRange n).splitBy fun i j => decide (D.block i = D.block j)
+
+@[simp]
+theorem flatten_blocks {n : ℕ} {x : Fin n → ℝ} (D : SignBlockDecomposition x) :
+    D.blocks.flatten = List.finRange n := by
+  simp [blocks]
+
+theorem nil_notMem_blocks {n : ℕ} {x : Fin n → ℝ}
+    (D : SignBlockDecomposition x) : [] ∉ D.blocks := by
+  exact List.nil_notMem_splitBy _ _
+
+theorem isChain_block_eq_of_mem_blocks {n : ℕ} {x : Fin n → ℝ}
+    (D : SignBlockDecomposition x) {B : List (Fin n)} (hB : B ∈ D.blocks) :
+    B.IsChain fun i j => D.block i = D.block j := by
+  simpa [blocks] using List.isChain_of_mem_splitBy hB
+
+theorem isChain_block_ne_blocks {n : ℕ} {x : Fin n → ℝ}
+    (D : SignBlockDecomposition x) :
+    D.blocks.IsChain fun A B =>
+      ∃ hA hB, D.block (A.getLast hA) ≠ D.block (B.head hB) := by
+  simpa [blocks] using
+    List.isChain_getLast_head_splitBy
+      (fun i j : Fin n => decide (D.block i = D.block j)) (List.finRange n)
+
+theorem same_block_of_between {n : ℕ} {x : Fin n → ℝ}
+    (D : SignBlockDecomposition x) {i j k : Fin n} (hik : i ≤ k) (hkj : k ≤ j)
+    (hij : D.block i = D.block j) : D.block k = D.block i := by
+  apply le_antisymm
+  · simpa [hij] using D.monotone_block hkj
+  · exact D.monotone_block hik
+
+theorem sign_eq_sign_of_block_eq {n : ℕ} {x : Fin n → ℝ}
+    (D : SignBlockDecomposition x) {i j : Fin n} (hi : x i ≠ 0) (hj : x j ≠ 0)
+    (hij : D.block i = D.block j) : SignType.sign (x i) = SignType.sign (x j) := by
+  rw [D.sign_eq_blockSign i hi, D.sign_eq_blockSign j hj, hij]
+
+end SignBlockDecomposition
+
+/-- Every nonzero finite real vector admits its canonical consecutive sign-block
+decomposition. Leading zeros are put in block zero, while an extension across
+internal zeros may put them in either adjacent block. -/
+theorem exists_signBlockDecomposition {n : ℕ} (x : Fin n → ℝ) (hx : x ≠ 0) :
+    Nonempty (SignBlockDecomposition x) := by
+  classical
+  let support : List (Fin n) :=
+    (List.finRange n).filter fun i => x i ≠ 0
+  have hx_exists : ∃ i, x i ≠ 0 := by
+    by_contra h
+    push Not at h
+    apply hx
+    funext i
+    exact h i
+  have hsupport_ne : support ≠ [] := by
+    obtain ⟨i, hi⟩ := hx_exists
+    intro hs
+    have himem : i ∈ support := by simp [support, hi]
+    rw [hs] at himem
+    simp at himem
+  have hsupport_sorted : support.SortedLT := by
+    exact ((List.sortedLT_finRange n).pairwise.filter _).sortedLT
+  let key : Fin n → SignType := fun i => SignType.sign (x i)
+  let d : List SignType := (support.map key).destutter (· ≠ ·)
+  obtain ⟨run, hrun_mono, hrun_surj, hrun_key⟩ :=
+    List.exists_monotone_destutter_index key support hsupport_ne
+  have hsigns :
+      support.map key =
+        ((List.ofFn x).map SignType.sign).filter (· ≠ 0) := by
+    simp only [support, key, List.ofFn_eq_map, List.map_map]
+    rw [List.filter_map]
+    congr 1
+    apply List.filter_congr
+    intro i hi
+    simp
+  have hd_ne : d ≠ [] := by
+    dsimp only [d]
+    intro hd
+    have hm : support.map key = [] :=
+      (List.destutter_eq_nil (R := fun s t : SignType => s ≠ t)).mp hd
+    exact hsupport_ne (by simpa using hm)
+  have hd_pos : 0 < d.length := by
+    exact Nat.pos_of_ne_zero (by simpa using hd_ne)
+  have hvariation : signVariations x = d.length - 1 := by
+    rw [signVariations, List.signVariations, ← hsigns]
+  have hcount : d.length = signVariations x + 1 := by
+    rw [hvariation]
+    lia
+  let supportIso : Fin support.length ≃o {i // i ∈ support} :=
+    hsupport_sorted.getIso support
+  let supportSet : Set (Fin n) := {i | x i ≠ 0}
+  let supportBlock : Fin n → Fin d.length := fun i =>
+    if hi : i ∈ support then
+      run (supportIso.symm ⟨i, hi⟩)
+    else
+      ⟨0, hd_pos⟩
+  have hpartial_mono : MonotoneOn supportBlock supportSet := by
+    intro i hi j hj hij
+    have hi0 : x i ≠ 0 := by simpa [supportSet] using hi
+    have hj0 : x j ≠ 0 := by simpa [supportSet] using hj
+    have himem : i ∈ support := by simp [support, hi0]
+    have hjmem : j ∈ support := by simp [support, hj0]
+    simp only [supportBlock, dif_pos himem, dif_pos hjmem]
+    apply hrun_mono
+    apply supportIso.symm.monotone
+    exact hij
+  letI : NeZero d.length := ⟨Nat.ne_of_gt hd_pos⟩
+  have hbelow : BddBelow (supportBlock '' supportSet) := by
+    refine ⟨⊥, ?_⟩
+    rintro _ ⟨i, hi, rfl⟩
+    exact bot_le
+  have habove : BddAbove (supportBlock '' supportSet) := by
+    refine ⟨⊤, ?_⟩
+    rintro _ ⟨i, hi, rfl⟩
+    exact le_top
+  obtain ⟨block, hblock_mono, hblock_eq⟩ :=
+    hpartial_mono.exists_monotone_extension hbelow habove
+  have hsupport_get_mem (i : Fin support.length) : support.get i ∈ support :=
+    List.get_mem support i
+  have hsupport_get_ne (i : Fin support.length) : x (support.get i) ≠ 0 := by
+    exact of_decide_eq_true (List.mem_filter.mp (hsupport_get_mem i)).2
+  have hsupportIso_symm_get (i : Fin support.length) :
+      supportIso.symm ⟨support.get i, hsupport_get_mem i⟩ = i := by
+    exact supportIso.symm_apply_apply i
+  have hd_get_ne (b : Fin d.length) : d.get b ≠ 0 := by
+    have hbmem : d.get b ∈ support.map key :=
+      (List.destutter_sublist
+        (R := fun s t : SignType => s ≠ t) (support.map key)).mem (List.get_mem d b)
+    obtain ⟨i, hi, hkey⟩ := List.mem_map.mp hbmem
+    rw [← hkey]
+    exact sign_ne_zero.mpr
+      (of_decide_eq_true (List.mem_filter.mp hi).2)
+  refine ⟨{
+    blockCount := d.length
+    blockCount_eq := hcount
+    block := block
+    monotone_block := hblock_mono
+    block_has_nonzero := ?_
+    blockSign := fun b => d.get b
+    blockSign_ne_zero := ?_
+    sign_eq_blockSign := ?_
+    adjacent_blockSign := ?_ }⟩
+  · intro b
+    obtain ⟨i, hi⟩ := hrun_surj b
+    have hne := hsupport_get_ne i
+    have himem := hsupport_get_mem i
+    refine ⟨support.get i, ?_, hne⟩
+    rw [← hblock_eq (by simpa [supportSet] using hne)]
+    rw [show supportBlock (support.get i) = run i by
+      simpa only [supportBlock, dif_pos himem] using
+        congrArg run (hsupportIso_symm_get i), hi]
+  · intro b
+    exact hd_get_ne b
+  · intro i hi
+    have himem : i ∈ support := by simp [support, hi]
+    let k : Fin support.length := supportIso.symm ⟨i, himem⟩
+    have hget : support.get k = i := by
+      have h := supportIso.apply_symm_apply ⟨i, himem⟩
+      exact congrArg Subtype.val h
+    have hblock : block i = run k := by
+      rw [← hblock_eq (by simpa [supportSet] using hi)]
+      simp [supportBlock, himem, k]
+    calc
+      SignType.sign (x i) = key (support.get k) := by
+        simpa only [key] using
+          (congrArg (fun j => SignType.sign (x j)) hget).symm
+      _ = d.get (run k) := hrun_key k
+      _ = d.get (block i) := by rw [hblock]
+  · intro i j hij
+    have hchain : d.IsChain (· ≠ ·) := by
+      exact List.isChain_destutter
+        (R := fun s t : SignType => s ≠ t) (support.map key)
+    have hne : d.get i ≠ d.get j := by
+      have hrel := List.isChain_iff_getElem.mp hchain i.val (by lia)
+      simpa [List.get_eq_getElem, hij] using hrel
+    exact SignType.eq_neg_of_ne_of_ne_zero
+      (hd_get_ne i) (hd_get_ne j)
+      hne
+
 /-- A finite vector split into a nonnegative initial block and a nonpositive
 final block has at most one sign variation. -/
 lemma signVariations_le_one_of_castAdd_nonneg_natAdd_nonpos {m n : ℕ}
diff --git a/RealRooted/Mathlib/LinearAlgebra/Matrix/VariationDiminishing.lean b/RealRooted/Mathlib/LinearAlgebra/Matrix/VariationDiminishing.lean
index e694e453..d85a440e 100644
--- a/RealRooted/Mathlib/LinearAlgebra/Matrix/VariationDiminishing.lean
+++ b/RealRooted/Mathlib/LinearAlgebra/Matrix/VariationDiminishing.lean
@@ -47,10 +47,9 @@ lemma Matrix.IsTotallyNonnegRect.aggregate_monotone
 ```
 
 This is the consecutive-block determinant expansion used in Chapter 5,
-Section 1.  It requires a finite Cauchy--Binet/multilinearity development not
-yet present in the local rectangular-TN API.  Until that lemma and the strict
-sector and limit lemmas in Steps 4--5 are proved, this file deliberately does
-not declare the full theorem with an unproved backend.
+Section 1.  The lemma is proved below by determinant multilinearity.  Until
+the strict sector and limit lemmas in Steps 4--5 are proved, this file
+deliberately does not declare the full theorem with an unproved backend.
 -/
 
 public section
@@ -69,6 +68,164 @@ end Fin
 
 namespace Matrix
 
+/-- Expanding a minor after fiberwise weighted column aggregation gives the
+sum of the corresponding source minors times their weight products. -/
+theorem det_submatrix_fiberwise_sum
+    {R ι ρ κ σ : Type*} [CommRing R]
+    [Fintype ι] [DecidableEq ι] [Fintype κ] [DecidableEq σ]
+    (M : Matrix ρ κ R) (rows : ι → ρ) (cols : ι → σ)
+    (block : κ → σ) (weight : κ → R) :
+    (Matrix.submatrix
+        ((fun i s ↦ ∑ j with block j = s, M i j * weight j) : Matrix ρ σ R)
+        rows cols).det =
+      ∑ r ∈ Fintype.piFinset
+          (fun s : ι ↦ Finset.univ.filter fun j ↦ block j = cols s),
+        (∏ s, weight (r s)) * (M.submatrix rows r).det := by
+  classical
+  let fibers : ι → Finset κ := fun s ↦
+    Finset.univ.filter fun j ↦ block j = cols s
+  let sourceCol : ι → κ → (ι → R) := fun _ j i ↦
+    M (rows i) j * weight j
+  have hexpand :
+      (Matrix.submatrix
+          ((fun i s ↦ ∑ j with block j = s, M i j * weight j) : Matrix ρ σ R)
+          rows cols).det =
+        ∑ r ∈ Fintype.piFinset fibers,
+          Matrix.det (fun s i ↦ sourceCol s (r s) i) := by
+    rw [← Matrix.det_transpose]
+    have hmatrix :
+        (Matrix.submatrix
+          ((fun i s ↦ ∑ j with block j = s, M i j * weight j) : Matrix ρ σ R)
+          rows cols)ᵀ =
+          fun s ↦ ∑ j ∈ fibers s, sourceCol s j := by
+      ext s i
+      simp [fibers, sourceCol]
+    rw [hmatrix]
+    change
+      (Matrix.detRowAlternating : (ι → R) [⋀^ι]→ₗ[R] R).toMultilinearMap
+          (fun s ↦ ∑ j ∈ fibers s, sourceCol s j) =
+        ∑ r ∈ Fintype.piFinset fibers,
+          (Matrix.detRowAlternating :
+            (ι → R) [⋀^ι]→ₗ[R] R).toMultilinearMap
+              (fun s ↦ sourceCol s (r s))
+    exact MultilinearMap.map_sum_finset
+      (Matrix.detRowAlternating :
+        (ι → R) [⋀^ι]→ₗ[R] R).toMultilinearMap
+      sourceCol fibers
+  rw [hexpand]
+  apply Finset.sum_congr rfl
+  intro r _
+  rw [← Matrix.det_transpose (M.submatrix rows r)]
+  simp only [sourceCol]
+  change
+    (Matrix.detRowAlternating : (ι → R) [⋀^ι]→ₗ[R] R).toMultilinearMap
+      (fun s i ↦ M (rows i) (r s) * weight (r s)) =
+    (∏ s, weight (r s)) *
+      (Matrix.detRowAlternating : (ι → R) [⋀^ι]→ₗ[R] R).toMultilinearMap
+        (fun s i ↦ M (rows i) (r s))
+  rw [show (fun s i ↦ M (rows i) (r s) * weight (r s)) =
+      (fun s ↦ weight (r s) • fun i ↦ M (rows i) (r s)) by
+    funext s i
+    simp [mul_comm]]
+  simpa only [smul_eq_mul] using
+    (MultilinearMap.map_smul_univ Matrix.detRowAlternating.toMultilinearMap
+      (fun s ↦ weight (r s)) (fun s i ↦ M (rows i) (r s)))
+
+/-- Aggregating columns along a monotone block map with nonnegative weights
+preserves rectangular total nonnegativity. -/
+lemma IsTotallyNonnegRect.aggregate_monotone
+    {m n q : ℕ} {M : Matrix (Fin m) (Fin n) ℝ}
+    (hM : M.IsTotallyNonnegRect) (block : Fin n → Fin q)
+    (hblock : Monotone block) (weight : Fin n → ℝ)
+    (hweight : ∀ j, 0 ≤ weight j) :
+    Matrix.IsTotallyNonnegRect
+      ((fun i s ↦ ∑ j with block j = s, M i j * weight j) :
+        Matrix (Fin m) (Fin q) ℝ) := by
+  classical
+  intro k rows cols hrows hcols
+  rw [det_submatrix_fiberwise_sum]
+  refine Finset.sum_nonneg fun r hr ↦ ?_
+  have hrblock : ∀ s, block (r s) = cols s := by
+    intro s
+    simpa using (Fintype.mem_piFinset.mp hr s)
+  have hrmono : StrictMono r := by
+    intro a b hab
+    by_contra hnlt
+    have hrle : r b ≤ r a := le_of_not_gt hnlt
+    have hblockle : block (r b) ≤ block (r a) := hblock hrle
+    rw [hrblock b, hrblock a] at hblockle
+    exact (not_le_of_gt (hcols hab)) hblockle
+  have hminor : 0 ≤ (M.submatrix rows r).det := hM hrows hrmono
+  have hprod : 0 ≤ ∏ s, weight (r s) :=
+    Finset.prod_nonneg fun s _ ↦ hweight (r s)
+  exact mul_nonneg hprod hminor
+
+/-- If every source minor of the target size is positive and every aggregation
+fiber has a positive-weight representative, then the aggregated maximal
+minors have a common strict sign. This is the strict-summand step in Karlin,
+Chapter 5, Section 1, Theorem 1.2. -/
+lemma strictMaximalMinors_aggregate_monotone
+    {m n q : ℕ} {M : Matrix (Fin m) (Fin n) ℝ}
+    (hM : M.IsTotallyNonnegRect)
+    (hminor :
+      ∀ ⦃rows : Fin q → Fin m⦄ ⦃cols : Fin q → Fin n⦄,
+        StrictMono rows → StrictMono cols →
+          0 < (M.submatrix rows cols).det)
+    (block : Fin n → Fin q) (hblock : Monotone block)
+    (weight : Fin n → ℝ) (hweight : ∀ j, 0 ≤ weight j)
+    (hfiber : ∀ s, ∃ j, block j = s ∧ 0 < weight j) :
+    ∀ ⦃rows rows' : Fin q → Fin m⦄,
+      StrictMono rows → StrictMono rows' →
+        0 <
+          (Matrix.submatrix
+              ((fun i s ↦ ∑ j with block j = s, M i j * weight j) :
+                Matrix (Fin m) (Fin q) ℝ) rows id).det *
+            (Matrix.submatrix
+              ((fun i s ↦ ∑ j with block j = s, M i j * weight j) :
+                Matrix (Fin m) (Fin q) ℝ) rows' id).det := by
+  classical
+  choose selector hselector_block hselector_weight using hfiber
+  have hselector_mono : StrictMono selector := by
+    intro a b hab
+    apply lt_of_not_ge
+    intro hba
+    have hle := hblock hba
+    rw [hselector_block a, hselector_block b] at hle
+    exact (not_le_of_gt hab) hle
+  have hselector_mem :
+      selector ∈ Fintype.piFinset
+        (fun s : Fin q ↦ Finset.univ.filter fun j ↦ block j = id s) := by
+    apply Fintype.mem_piFinset.mpr
+    intro s
+    simpa using hselector_block s
+  have hdet_pos (rows : Fin q → Fin m) (hrows : StrictMono rows) :
+      0 <
+        (Matrix.submatrix
+          ((fun i s ↦ ∑ j with block j = s, M i j * weight j) :
+            Matrix (Fin m) (Fin q) ℝ) rows id).det := by
+    rw [det_submatrix_fiberwise_sum]
+    apply Finset.sum_pos'
+    · intro r hr
+      have hrblock : ∀ s, block (r s) = s := by
+        intro s
+        simpa using (Fintype.mem_piFinset.mp hr s)
+      have hrmono : StrictMono r := by
+        intro a b hab
+        apply lt_of_not_ge
+        intro hba
+        have hle := hblock hba
+        rw [hrblock a, hrblock b] at hle
+        exact (not_le_of_gt hab) hle
+      exact mul_nonneg
+        (Finset.prod_nonneg fun s _ ↦ hweight (r s))
+        (hM hrows hrmono)
+    · refine ⟨selector, hselector_mem, ?_⟩
+      exact mul_pos
+        (Finset.prod_pos fun s _ ↦ hselector_weight s)
+        (hminor hrows hselector_mono)
+  intro rows rows' hrows hrows'
+  exact mul_pos (hdet_pos rows hrows) (hdet_pos rows' hrows')
+
 /-- A common nonzero sign for all maximal minors makes multiplication by the
 rectangular matrix injective. This is the rank step in Karlin, Chapter 5,
 Section 1, Theorem 1.1. -/
@@ -208,6 +365,77 @@ theorem signVariations_mulVec_le_card_sub_one_of_strictMaximalMinors
         (Fin.exists_strictMono_strictlyAlternates_of_le_signVariations
           hq hlarge)
 
+/-- A totally nonnegative rectangular matrix with all square minors strictly
+positive is variation diminishing in the local `S^-` convention. This follows
+Karlin, Chapter 5, Section 1, Theorem 1.2: aggregate consecutive sign blocks,
+apply Theorem 1.1 to the aggregate, and use the block count. -/
+theorem IsTotallyNonnegRect.signVariations_mulVec_le_of_posMinors
+    {m n : ℕ} {M : Matrix (Fin m) (Fin n) ℝ}
+    (hM : M.IsTotallyNonnegRect)
+    (hminor :
+      ∀ ⦃q : ℕ⦄ ⦃rows : Fin q → Fin m⦄ ⦃cols : Fin q → Fin n⦄,
+        StrictMono rows → StrictMono cols →
+          0 < (M.submatrix rows cols).det)
+    (x : Fin n → ℝ) :
+    Fin.signVariations (M.mulVec x) ≤ Fin.signVariations x := by
+  classical
+  by_cases hx : x = 0
+  · subst x
+    simp [Matrix.mulVec, dotProduct]
+  obtain ⟨D⟩ := Fin.exists_signBlockDecomposition x hx
+  let weight : Fin n → ℝ := fun j ↦ |x j|
+  let blockSign : Fin D.blockCount → ℝ := fun s ↦ D.blockSign s
+  let A : Matrix (Fin m) (Fin D.blockCount) ℝ :=
+    fun i s ↦ ∑ j with D.block j = s, M i j * weight j
+  have hfactor (j : Fin n) :
+      weight j * blockSign (D.block j) = x j := by
+    change |x j| * (D.blockSign (D.block j) : ℝ) = x j
+    by_cases hj : x j = 0
+    · simp [hj]
+    · rw [← D.sign_eq_blockSign j hj]
+      exact abs_mul_sign (x j)
+  have hmul : A.mulVec blockSign = M.mulVec x := by
+    ext i
+    rw [Matrix.mulVec, Matrix.mulVec, dotProduct, dotProduct]
+    simp only [A, Finset.sum_mul]
+    calc
+      (∑ s, ∑ j with D.block j = s,
+          M i j * weight j * blockSign s) =
+          ∑ s, ∑ j with D.block j = s, M i j * x j := by
+        apply Finset.sum_congr rfl
+        intro s _
+        apply Finset.sum_congr rfl
+        intro j hj
+        have hjblock : D.block j = s := (Finset.mem_filter.mp hj).2
+        rw [← hjblock, mul_assoc, hfactor]
+      _ = ∑ j, M i j * x j := by
+        simpa using
+          (Finset.sum_fiberwise Finset.univ D.block
+            (fun j ↦ M i j * x j))
+  have hfiber : ∀ s, ∃ j, D.block j = s ∧ 0 < weight j := by
+    intro s
+    obtain ⟨j, hjblock, hj⟩ := D.block_has_nonzero s
+    exact ⟨j, hjblock, by simpa [weight] using abs_pos.mpr hj⟩
+  have hAminor :
+      ∀ ⦃rows rows' : Fin D.blockCount → Fin m⦄,
+        StrictMono rows → StrictMono rows' →
+          0 < (A.submatrix rows id).det * (A.submatrix rows' id).det := by
+    simpa only [A] using
+      strictMaximalMinors_aggregate_monotone hM
+        (fun ⦃rows cols⦄ hrows hcols ↦
+          hminor (rows := rows) (cols := cols) hrows hcols)
+        D.block D.monotone_block weight (fun j ↦ abs_nonneg (x j)) hfiber
+  by_cases hqm : D.blockCount ≤ m
+  · have hout :=
+      signVariations_mulVec_le_card_sub_one_of_strictMaximalMinors
+        hqm hAminor blockSign
+    rw [hmul] at hout
+    simpa [D.blockCount_eq] using hout
+  · have hcard := Fin.signVariations_le_card_sub_one (M.mulVec x)
+    have hlt : m < D.blockCount := Nat.lt_of_not_ge hqm
+    rw [D.blockCount_eq] at hlt
+    lia
+
 /-- A totally nonnegative rectangular matrix sends a nonnegative vector to a
 nonnegative vector.  This is the positive one-block sector of the forward
 variation-diminishing argument. -/