Formalize Karlin's consecutive sign-block aggregation

[PerAlexandersson]

Source

S. Karlin, Total Positivity, Vol. I, Chapter V, §1, Theorem 1.2.

This follows the strict maximal-minor sector tracked in #288 and implemented in draft PR #289.
It is the next source step toward Theorems 1.3–1.4 and the forward ASW application.

Exact source construction

For a nonzero input vector x, let p = Fin.signVariations x.

1. Partition the ordered nonzero coordinates into exactly p + 1 maximal same-sign runs.

2. Extend those runs to a monotone total block label on all coordinates, assigning zero coordinates
   without creating empty blocks.

3. For each block k, form the aggregate column

   v^k = sum_{j in block k} |x_j| u^j.
   

4. Expand every aggregate maximal minor by determinant multilinearity over one source-column
   choice from each block.

5. Monotonicity and consecutive fibers make every chosen source tuple strictly increasing.

6. Strict sign regularity gives every nonzero summand one common sign; each block contains a
   nonzero coefficient, so at least one summand is nonzero.

7. Apply the strict maximal-minor theorem from Prove Karlin strict maximal-minor variation bound #289 to the aggregate matrix and alternating
   coefficient vector.

Smallest missing Lean layer

Sign blocks

Use List.splitBy on the ordered nonzero support. First prove the generic bridge

List.filterMap_head?_splitBy_key_eq_destutter

and then a source-facing decomposition such as

Fin.SignBlockDecomposition x
Fin.exists_signBlockDecomposition

with a monotone block map, nonzero witness in each block, same-sign coefficients inside each
fiber, and alternating adjacent block signs.

Determinant expansion

Prove a generic simultaneous column-choice expansion:

Matrix.det_column_choice_sum

for a matrix whose k-th column is a finite weighted sum of source columns. The existing
det_updateCol_sum does not provide this independent choice expansion.

Add the order lemma that a choice from strictly increasing fibers of a monotone block map is
strictly increasing.

Acceptance criteria

• The block count is connected to the existing Fin.signVariations; no parallel variation
  definition is introduced.
• The aggregate determinant expansion and strict common-sign conclusion have checked proofs.
• Karlin's Theorem 1.2 S^- consequence is derived from Prove Karlin strict maximal-minor variation bound #289's strict theorem.
• No variation-diminishing or real-rootedness conclusion is hidden behind a
  def ...Statement : Prop.
• The proof follows Karlin's consecutive-column aggregation rather than a guessed replacement.

[PerAlexandersson]

Direct source check against Karlin, Total Positivity I, Ch. V, §1, Theorem 1.2(a) (printed pp. 219–220) sharpens the implementation contract:

1. Let (p=S^-(c)). Split the coordinates into exactly (p+1) consecutive groups, each containing a nonzero coordinate, with weak signs alternating by group.
2. For each group define the aggregate column (v_k=sum |c_j|u^j). Then (Uc=sum_k(-1)^{k+1}v_k).
3. Expand every ((p+1))-minor of (V=(v_1,ldots,v_{p+1})) multilinearly. Every summand has the sign of the corresponding ((p+1))-minor of (U), and at least one summand has a strictly positive coefficient because each block contains a nonzero coordinate.
4. Hence (V) is strictly sign-consistent of order (p+1). Apply Theorem 1.1(a) to obtain (S^+(Uc)le p=S^-(c)). If (nle p+1), Karlin treats the bound as immediate.

For the ASW/TNN route, the exact positive-minor specialization is sufficient: prove positivity of the relevant order-((p+1)) minors of the approximating matrix, use nonnegative absolute weights and the same strict witness term, then invoke Matrix.signVariations_mulVec_le_card_sub_one_of_strictMaximalMinors from PR #289. No alternative proof route is intended.

This also shows why V.1.1 alone cannot update the tactics: the missing input is strict positivity at the dynamically chosen order (p+1), followed later by Karlin V.1.3–V.1.4 for the weak/rank case.

[PerAlexandersson]

Further direct source/API correction:

• Fin.signVariations is Karlin's (S^-): it deletes zero entries before counting changes. The project normalizes the zero vector to 0, rather than Karlin's exceptional value (-1).
• PR Prove Karlin strict maximal-minor variation bound #289's theorem is consequently the (S^-) strict-maximal-minor bound. It is not the full (S^+) statement printed as Karlin V.1.1(a).
• This weaker sector is nevertheless exactly sufficient for the ASW proof. In Karlin VIII §3, Theorem 3.1 (printed pp. 398–399), the key application is
  [
  nr-1=S^-(y^)le S^-(x^0+x^)
  ]
  for the totally positive matrix (M_n), followed by a direct bound on (S^-(x^0+x^*)). No (S^+) count is used there.
• The displayed Matrix.IsTotallyNonnegRect.aggregate_monotone near the start of VariationDiminishing.lean is currently only a declaration shown in a module doc comment, not implemented Lean API.

So the source-faithful ASW chain is: implement the (S^-) positive-minor V.1.2 specialization; obtain the weak/rank (S^-) transformation theorem by V.1.3–V.1.4; then reproduce VIII.3's perturbation argument. We should not claim the full (S^+) theorem unless a separate maximum-sign-variation notion is added.

[PerAlexandersson]

Lean implementation outline for Karlin's strict witness step, now that the two foundations are concrete:

1. Extract the local hexpand calculation from aggregate_monotone into a reusable determinant identity of the form
   [
   det(B[mathrm{rows},mathrm{cols}])
   = sum_{rinprod_s mathrm{fiber}(mathrm{cols}(s))}
   left(prod_s w_{r(s)}
   ight)det(M[mathrm{rows},r]).
   ]
   This is exactly Karlin's multilinear expansion, not an alternative argument.
2. Derive IsTotallyNonnegRect.aggregate_monotone from that identity: monotonicity of the block map and strict monotonicity of selected aggregate columns force every choice function (r) to be strictly monotone, so every source minor and every weight product is nonnegative.
3. For the maximal-minor strict lemma, choose one nonzero coordinate from each block using
   SignBlockDecomposition.block_has_nonzero. With weights |x j|, that chosen product is strictly positive. The same monotonicity argument makes the chosen source columns strictly increasing. If source minors of this order are positive, the selected summand is positive while all others are nonnegative, hence every aggregate maximal minor is positive.
4. Apply the positive-minor specialization of PR Prove Karlin strict maximal-minor variation bound #289's
   Matrix.signVariations_mulVec_le_card_sub_one_of_strictMaximalMinors.

The determinant identity should be public and Mathlib-shaped; the TNN and strict consequences should share it rather than carrying two copies of the multilinearity proof.

[PerAlexandersson]

Karlin V.1.2 is now implemented on stacked draft PR #291 in three source-ordered pieces:

• Matrix.det_submatrix_fiberwise_sum (ccc9c0d): the determinant multilinearity identity over an arbitrary CommRing; Axle 5092275a-6821-428d-a421-c8e5adab2471.
• Matrix.strictMaximalMinors_aggregate_monotone (a9a4adb): all summands nonnegative plus one positive-weight selector per fiber gives the strict maximal-minor product required by V.1.1; Axle 936a211d-c429-4290-b0a1-ac903156f5de.
• Matrix.IsTotallyNonnegRect.signVariations_mulVec_le_of_posMinors (360a034): exact V.1.2 assembly using SignBlockDecomposition, weights |x_j|, cast block signs, abs_mul_sign, Finset.sum_fiberwise, V.1.1, and the row-cardinality fallback; Axle 9cf16970-5719-4534-bdb5-95b4f6832596.

The PR remains draft/stacked and comparator CI is still running. This is not yet being reported as merged or accepted. No tactic changes are justified by this strict-stage result; ASW still needs Karlin V.1.3–V.1.4 to pass from strict positivity to the TNN matrix.

[PerAlexandersson]

V.1.1 is now merged on main as 9e20e54. PR #291 has been rebased to preserve only its five V.1.2 commits, retargeted to main, and force-pushed at 1dc6287. Because the automatic post-rebase run was cancelled by workflow concurrency, Comparator run 30751535569 and Lean Action run 30751536435 were dispatched explicitly against that exact SHA and are in progress.

[PerAlexandersson]

A read-only proof-golf audit of PR #291 found a small deduplication path for
Fin.exists_signBlockDecomposition without changing its signature or the
Fin.SignBlockDecomposition API:

• introduce one local mem_support_iff (i) : i ∈ support ↔ x i ≠ 0 and replace repeated
  support/nonzero simpa conversions with it;
• define and reuse hsupport_get_ne for support.get values;
• factor the repeated block/support agreement into
  block_eq_run_of_mem {i} (hi : i ∈ support) and use it in both block_has_nonzero and
  sign_eq_blockSign;
• retain the named structure literal and fill blockSign := d.get and
  blockSign_ne_zero := hd_get_ne directly rather than using a positional constructor.

This was notes-only; no files were edited and no build was run.