Formalize Karlin's weak sign-regular variation-diminishing theorem

[PerAlexandersson]

Source

Karlin, Total Positivity, Vol. I, Chapter V, §1, Theorem 1.4 (printed p. 223).

For a sign-regular matrix U of rank r, the forward theorem is

S⁻(Uc) ≤ min(r - 1, S⁻(c)).

The source says this follows from Theorem 1.3 exactly as the strict sign-block theorem V.1.2 follows from V.1.1. The converse under full column rank belongs to a later dependency and is not required for the initial ASW forward route.

Required source proof route

1. Depend on the completed V.1.3 rank-sensitive sign-consistent theorem; do not assume the rank bound separately.
2. Split c into S⁻(c)+1 consecutive nonempty same-sign blocks using Fin.SignBlockDecomposition.
3. Aggregate columns with weights |c_j|, exactly as in V.1.2, and express Uc as the aggregate matrix applied to the cast block-sign vector.
4. Use sign-regularity of U, determinant multilinearity, and the existing fiberwise determinant expansion to prove that the aggregate matrix is sign-consistent of the relevant order. In the weak case summands may vanish; no positive-selector hypothesis is available or required.
5. Apply V.1.3 to the aggregate matrix to obtain the S⁻(c) bound. Apply V.1.3 directly to U for the rank U - 1 bound, then combine them with min.
6. Translate the project convention S⁻(0)=0 explicitly.

Proposed main declaration

theorem Matrix.IsSignRegular.signVariations_mulVec_le
    {m n r : ℕ} {U : Matrix (Fin n) (Fin m) ℝ}
    (hU : U.IsSignRegular)
    (hrank : Module.finrank ℝ (LinearMap.range U.mulVecLin) = r)
    (c : Fin m → ℝ) :
    Fin.signVariations (U.mulVec c) ≤
      min (r - 1) (Fin.signVariations c) := by
  ...

IsSignRegular should be a genuine reusable property definition quantifying the common weak sign of minors of every order; it must not be a theorem placeholder.

Acceptance criteria

• Follows the paper’s V.1.3 → V.1.4 sign-block route.
• Reuses Matrix.det_submatrix_fiberwise_sum and Fin.SignBlockDecomposition.
• No sorry, axioms, or theorem-shaped def ...Statement : Prop.
• Proves both components of the min bound.
• Strong enough to replace the ASW forward variation-diminishing assumption after the Toeplitz matrix is shown TNN/sign-regular.
• Focused and full CI are green.