Refactor threshold matrix theorem layers

ARCHITECTURE.md

@@ -372,6 +372,23 @@ umbrella imports only `BasicRules`, exactly matching the sequence tactics it
 advertises and preserving its 425-module budget; the full tactic umbrella
 continues to re-export the complete compatibility facade.
 
+Threshold matrices now have a theorem-layer boundary of their own:
+
+- `AffineProperPosition` owns the constant and positive-slope affine facts
+  shared with the Veronese matrix development;
+- `ThresholdMatrix.Basic` owns threshold entries, rows, matrix preservation,
+  and the finite-entry helper interface;
+- `ThresholdMatrix.HaglundZhang` owns the Haglund--Zhang backend and A046802
+  surface;
+- `ThresholdMatrix.GustafssonSolus` owns the independent Gustafsson--Solus
+  row-choice backend; and
+- `ThresholdMatrix` remains the historical compatibility facade.
+
+The three implementation layers have 247, 1,124, and 778 local lines in place
+of one 2,140-line mixed source. Direct application consumers stop at their
+own child module. `AffineProperPosition` also removes the former dependency
+from the generic threshold layer to the full Veronese application.
+
 `Tactic.OEIS` is undergoing the same certificate-family migration. Its
 `OEIS.Basic` child owns the scalar-denominator certificate aliases, and
 `OEIS.DerivativeLag` owns the degree-two derivative-lag parser, dispatch, and

README.md

@@ -99,9 +99,13 @@ emulation. These scripts complement `lake build`; they do not replace it.
   definitions, `f`-polynomial transport, symmetric-decomposition, and Theorem
   2.6 layers; `SymmetricDecomposition.lean` remains their compatibility
   import. `Bezoutian.lean` contains the classical Bezoutian interface.
-- `RealRooted/RowThreshold.lean` and `ThresholdMatrix.lean` contain
-  row-threshold and threshold-matrix preservers, including the
-  Gustafsson-Solus and Haglund-Zhang/A046802 backends.
+- `RealRooted/RowThreshold.lean` contains the row-threshold preserver.
+  `ThresholdMatrix/Basic.lean` owns the generic threshold-matrix API,
+  while its `HaglundZhang` and `GustafssonSolus` children own the two
+  independent application backends. `ThresholdMatrix.lean` remains their
+  compatibility import. Shared constant and positive-slope affine
+  proper-position lemmas live in `AffineProperPosition.lean` rather than in a
+  Veronese-specific module.
 - `RealRooted/NarayanaTransformation/` layers the Mao--Wang Narayana
   transformation by root geometry, basis transforms, factorial preservation,
   coefficient identities, rectangular convolution, recurrences, and endpoints;

RealRooted.lean

@@ -21,6 +21,7 @@ import RealRooted.AffineFamily.LowDegree
 import RealRooted.AffineFamily.PositiveFamily
 import RealRooted.AffineFamily.RootCrossing
 import RealRooted.AffineFamily.Wronskian
+import RealRooted.AffineProperPosition
 import RealRooted.AissenSchoenbergWhitney
 import RealRooted.AissenSchoenbergWhitneyBase
 import RealRooted.AllCombo
@@ -829,6 +830,9 @@ import RealRooted.Tactic.WagnerX.Syntax
 import RealRooted.Tactic.WagnerX.TranslatedLag
 import RealRooted.Tactic.WeightedSum
 import RealRooted.ThresholdMatrix
+import RealRooted.ThresholdMatrix.Basic
+import RealRooted.ThresholdMatrix.GustafssonSolus
+import RealRooted.ThresholdMatrix.HaglundZhang
 import RealRooted.Touchard
 import RealRooted.TridiagonalDet
 import RealRooted.UpperDerivativeInterlace

RealRooted/AffineProperPosition.lean

@@ -0,0 +1,97 @@
+import RealRooted.AffineFamily
+
+/-!
+# Proper position for affine polynomials
+
+Elementary proper-position lemmas for constants and positive-slope affine
+polynomials.  These facts are shared by the Veronese and threshold-matrix
+developments, so they live below both application layers.
+-/
+
+open Polynomial
+
+noncomputable section
+
+namespace RealRooted
+
+/-- Any two constant polynomials are in zero-aware proper position. -/
+lemma prec0_C_C (a b : ℝ) : Prec0 (C a : ℝ[X]) (C b : ℝ[X]) := by
+  by_cases ha : a = 0
+  · left
+    simp [ha]
+  by_cases hb : b = 0
+  · right
+    simp_all
+  right
+  right
+  have hCa : (C a : ℝ[X]) ≠ 0 := C_ne_zero.mpr ha
+  have hCb : (C b : ℝ[X]) ≠ 0 := C_ne_zero.mpr hb
+  have hrr_a : ((C a : ℝ[X]) ≠ 0 ∧ (C a : ℝ[X]).Splits) :=
+    isRealRooted_of_deg_zero hCa (by simp)
+  have hrr_b : ((C b : ℝ[X]) ≠ 0 ∧ (C b : ℝ[X]).Splits) :=
+    isRealRooted_of_deg_zero hCb (by simp)
+  refine ⟨hrr_a, hrr_b, [], [], by simp, by simp, by simp, by simp, ?_⟩
+  exact Or.inr ⟨by lia, by simp [ListAlternates]⟩
+
+/-- Factoring out `X` after adding it to an affine multiple of `X`. -/
+lemma affine_mul_X_add_X_eq (s t : ℝ) :
+    ((C s * X + C t) * X + X : ℝ[X]) =
+      X * (C s * X + C (t + 1)) := by
+  grind
+
+/-- The polynomial obtained by adding `X` to a positive-slope affine multiple
+of `X` is nonzero and real-rooted. -/
+lemma isRealRooted_affine_mul_X_add_X {s t : ℝ} (hs : 0 < s) :
+    (((C s * X + C t) * X + X : ℝ[X]) ≠ 0 ∧
+      ((C s * X + C t) * X + X : ℝ[X]).Splits) := by
+  rw [affine_mul_X_add_X_eq]
+  exact isRealRooted_X_mul
+    (isRealRooted_affine_factor (s := s) (t := t + 1) hs).1
+    (isRealRooted_affine_factor (s := s) (t := t + 1) hs).2
+
+/-- A cross-product inequality orders the roots of two positive-slope affine
+polynomials. -/
+lemma affineLinear_root_le_of_cross {u v U V : ℝ}
+    (hu : 0 < u) (hU : 0 < U) (hcross : u * V ≤ U * v) :
+    -(u⁻¹ * v) ≤ -(U⁻¹ * V) := by
+  rw [neg_le_neg_iff]
+  rw [← div_eq_inv_mul, ← div_eq_inv_mul]
+  rw [div_le_div_iff₀ hU hu]
+  grind
+
+/-- Positive-slope affine polynomials are in proper position when their
+coefficient cross product has the corresponding order. -/
+lemma prec_affine_linear_affine_linear_of_cross
+    {u v U V : ℝ} (hu : 0 < u) (hU : 0 < U)
+    (hcross : u * V ≤ U * v) :
+    Prec (C u * X + C v) (C U * X + C V) := by
+  have hroot : -(u⁻¹ * v) ≤ -(U⁻¹ * V) :=
+    affineLinear_root_le_of_cross hu hU hcross
+  have hp_nat : (C u * X + C v : ℝ[X]).natDegree = 1 := by grind
+  have hq_nat : (C U * X + C V : ℝ[X]).natDegree = 1 := by grind
+  have hp_rr : ((C u * X + C v : ℝ[X]) ≠ 0 ∧ (C u * X + C v : ℝ[X]).Splits) :=
+    isRealRooted_affine_factor (s := u) (t := v) hu
+  have hq_rr : ((C U * X + C V : ℝ[X]) ≠ 0 ∧ (C U * X + C V : ℝ[X]).Splits) :=
+    isRealRooted_affine_factor (s := U) (t := V) hU
+  have hp_deg : (C u * X + C v : ℝ[X]).degree = 1 := by
+    rw [degree_eq_natDegree hp_rr.1, hp_nat]
+    lia
+  have hq_deg : (C U * X + C V : ℝ[X]).degree = 1 := by
+    rw [degree_eq_natDegree hq_rr.1, hq_nat]
+    lia
+  refine ⟨hp_rr, hq_rr, [-(u⁻¹ * v)], [-(U⁻¹ * V)], by simp, by simp, ?_, ?_, ?_⟩
+  · simpa [hp_deg] using
+      (Polynomial.roots_degree_eq_one (p := (C u * X + C v : ℝ[X])) hp_deg).symm
+  · simpa [hq_deg] using
+      (Polynomial.roots_degree_eq_one (p := (C U * X + C V : ℝ[X])) hq_deg).symm
+  · exact Or.inr ⟨by simp, by simpa [ListAlternates, ListInterlaces] using hroot⟩
+
+/-- Zero-aware form of
+`prec_affine_linear_affine_linear_of_cross`. -/
+lemma prec0_affine_linear_affine_linear_of_cross
+    {u v U V : ℝ} (hu : 0 < u) (hU : 0 < U)
+    (hcross : u * V ≤ U * v) :
+    Prec0 (C u * X + C v) (C U * X + C V) :=
+  (prec_affine_linear_affine_linear_of_cross hu hU hcross).toPrec0
+
+end RealRooted

RealRooted/GarloffWagner/Theorem12.lean

@@ -159,23 +159,6 @@ theorem prec0_C_mul_left_of_nonneg {f g : ℝ[X]}
   · simpa [hg0] using prec0_zero_right (C a * f)
   · exact (prec_C_mul_left hprec ha_pos.ne').toPrec0
 
-/-- Adding two nonnegative-coefficient left summands with a common right bound
-preserves zero-aware proper position. -/
-theorem prec0_add_left_of_common_right_of_nonneg {p q h : ℝ[X]}
-    (hph : Prec0 p h) (hqh : Prec0 q h)
-    (hpnn : HasNonnegCoeffs p) (hqnn : HasNonnegCoeffs q) :
-    Prec0 (p + q) h := by
-  classical
-  have hsum :
-      (Finset.univ.sum (fun b : Bool => cond b p q)) = p + q := by
-    simp
-  rw [← hsum]
-  apply prec0_finsetSum_right_of_nonneg
-  · intro b _
-    cases b <;> simp [hph, hqh]
-  · intro b _
-    cases b <;> simp [hpnn, hqnn]
-
 theorem HasNonnegCoeffs.weightedSum :
     ∀ l : List (ℝ × ℝ[X]),
       (∀ ap ∈ l, 0 ≤ ap.1) →

RealRooted/GustafssonSolus.lean

@@ -1,4 +1,4 @@
-import RealRooted.ThresholdMatrix
+import RealRooted.ThresholdMatrix.GustafssonSolus
 
 /-!
 # Gustafsson--Solus interlacing recursion

RealRooted/OEIS/A046802.lean

@@ -1,10 +1,10 @@
-import RealRooted.ThresholdMatrix
+import RealRooted.ThresholdMatrix.HaglundZhang
 
 /-!
 # OEIS A046802
 
 This module is the sequence-facing surface for the A046802 backend.  The
-mathematical work lives in `RealRooted.ThresholdMatrix`, where the
+mathematical work lives in `RealRooted.ThresholdMatrix.HaglundZhang`, where the
 Haglund--Zhang binomial Eulerian refined vector is encoded as a threshold
 matrix recursion and the reusable interlacing backend is proved.
 

RealRooted/PFPolynomial.lean

@@ -493,6 +493,23 @@ theorem prec0_add_right_of_common_left_of_nonneg {p q r : ℝ[X]}
       (by
         simp_all)
 
+/-- Fixed-right cone closure in the two-summand form used downstream:
+if two nonnegative-coefficient summands have a common right interleaver, their
+sum has that same right interleaver. -/
+theorem prec0_add_left_of_common_right_of_nonneg {p q h : ℝ[X]}
+    (hph : Prec0 p h) (hqh : Prec0 q h)
+    (hpnn : HasNonnegCoeffs p) (hqnn : HasNonnegCoeffs q) :
+    Prec0 (p + q) h := by
+  classical
+  have hsum : Finset.univ.sum (fun b : Bool ↦ cond b p q) = p + q := by
+    simp
+  rw [← hsum]
+  apply prec0_finsetSum_right_of_nonneg
+  · intro b _
+    cases b <;> simp [hph, hqh]
+  · intro b _
+    cases b <;> simp [hpnn, hqnn]
+
 /-- Fixed-left cone closure for two nonnegative scalar multiples. -/
 theorem prec0_nonneg_combo_right_of_common_left_of_nonneg {p q r : ℝ[X]}
     (hpq : Prec0 p q) (hpr : Prec0 p r)

RealRooted/RowThresholdOne.lean

@@ -1,4 +1,4 @@
-import RealRooted.ThresholdMatrix
+import RealRooted.ThresholdMatrix.Basic
 import RealRooted.VeroneseMatrix
 
 open Polynomial
@@ -39,28 +39,13 @@ theorem thresholdEntry_one (t j : ℕ) :
   unfold thresholdEntry
   split_ifs <;> simp_all
 
-/-- Reflexivity of `Prec0` on real-rooted polynomials. -/
-theorem prec0_refl_of_realRooted {p : ℝ[X]} (hp : p ≠ 0 ∧ p.Splits) : Prec0 p p :=
-  (prec_refl hp.1 hp.2).toPrec0
-
 /-- `X * (C s * X + C v)` is real-rooted for positive `s`. -/
 theorem isRealRooted_X_mul_affine {s v : ℝ} (hs : 0 < s) :
     (X * (C s * X + C v)) ≠ 0 ∧ (X * (C s * X + C v)).Splits := by
   obtain ⟨hne, hsplits⟩ := isRealRooted_affine_factor (s := s) (t := v) hs
   refine ⟨mul_ne_zero isRealRooted_X.1 hne, ?_⟩
   exact isRealRooted_X.2.mul hsplits
 
-/-- Degree-one to degree-two step: a positive affine form precedes the
-`X`-multiple of another one under the cross inequality. -/
-theorem prec0_affine_to_X_mul_affine {u v U V : ℝ}
-    (hu : 0 < u) (hU : 0 < U) (hcross : u * V ≤ U * v)
-    (hv : 0 ≤ v) (hV : 0 ≤ V) :
-    Prec0 (C U * X + C V) (X * (C u * X + C v)) :=
-  (prec_to_prec_mul_X_of_nonneg
-    (prec_affine_linear_affine_linear_of_cross hu hU hcross)
-    (hasNonnegCoeffs_affine_linear hu.le hv)
-    (hasNonnegCoeffs_affine_linear hU.le hV)).toPrec0
-
 /-! ### The six entry patterns -/
 
 private theorem case_XXXX {s t : ℝ} (hs : 0 < s) :