Prove Karlin's strict maximal-minor variation-diminishing theorem

[PerAlexandersson]

Source

S. Karlin, Total Positivity, Vol. I:

• Chapter V, §1, Theorems 1.1--1.4: finite variation-diminishing theory.
• Chapter V, §1, Lemma 1.1, Proposition 1.2, and Theorem 1.3: approximation and rank-deficient/non-strict reductions.
• Chapter VIII, §3, Theorem 3.1: the Aissen--Schoenberg--Whitney application.

This is a continuation of #241. The base cases are already checked in
RealRooted/Mathlib/LinearAlgebra/Matrix/VariationDiminishing.lean.

Exact next theorem

Prove the strict full-column-rank sector first:

Matrix.signVariations_mulVec_le_card_sub_one_of_strictMaximalMinors

For a finite real matrix with q columns, if all maximal minors are nonzero
and have the same sign, prove that every vector with maximal sign variation
has nonzero image and

signVariations (A *ᵥ x) ≤ q - 1.

This is the weakened S⁻ consequence needed by the repository; Karlin proves
the stronger S⁺ formulation.

Paper-derived proof order

1. Formalize the strict maximal-minor argument from Chapter V, §1.
2. Add the monotone aggregation/block decomposition used in Karlin's proof.
3. Extend from the strict sector to totally nonnegative matrices via the
   approximation and rank-deficiency steps in Chapter V, §1, Lemma 1.1,
   Proposition 1.2, and Theorem 1.3.
4. Apply the resulting finite variation-diminishing theorem to the Toeplitz
   truncations in Chapter VIII, §3 to finish the forward ASW implication.

Chapter V, §3, Theorem 3.1 is an integral-kernel reduction and is not the
source for the non-strict finite-matrix approximation step.

Acceptance criteria

• The strict maximal-minor theorem above has a checked Lean proof.
• Any combinatorial matrix interpretation that is intentionally assumed is
  exposed as an explicit hypothesis with a nearby comment explaining the
  boundary.
• Variation diminution, total nonnegativity consequences, and
  real-rootedness are proved, not hidden behind a def ...Statement : Prop.
• The proof follows Karlin's order; alternative guessed routes should not be
  substituted without first documenting why the cited argument cannot be
  formalized.

[PerAlexandersson]

Source/API reconciliation completed against Karlin, Total Positivity, Vol. I, Chapter V, §1 (printed pp. 217–222; cached scan pp. 229–234).

The exact first proof target is Theorem 1.1, not aggregation:

1. From q ≤ S⁻(A x) with q > 0, extract q+1 increasing output rows with strict alternating signs.
2. Restrict A to those rows.
3. Form the alternating vector of row-deletion maximal minors.
4. Laplace expansion gives that this vector lies in the kernel of the restricted matrix transpose.
5. The common nonzero sign of all maximal minors makes the cofactor vector alternate strictly, so its pointwise product with the selected output has one strict sign.
6. Its sum is therefore nonzero, contradicting the transpose-kernel identity.

The generic cofactor identity is now implemented on the clean work branch as Matrix.transpose_mulVec_alternating_det_submatrix_succAbove; Axle 4.31 accepted the isolated declaration. The sign-variation witness helper is being proved next. No aggregation, approximation, or full ASW conclusion is being assumed.

Karlin Theorem 1.2’s consecutive-column sign-block aggregation comes only after this strict sector; Theorems 1.3–1.4 then handle weak/rank-deficient cases.