Formalize Karlin's rank-sensitive sign-consistent variation bound

[PerAlexandersson]

Source

Karlin, Total Positivity, Vol. I, Chapter V, §1, Theorem 1.3 and Propositions 1.1–1.2 (printed pp. 220–222).

The source theorem states: if U is an n × m matrix of rank r and is sign-consistent of order r (SC_r), then S⁻(Uc) ≤ r - 1 for every c. If U is strictly sign-consistent of order r (SSC_r) and c ≠ 0, then the source also gives the corresponding S⁺ bound. The project currently uses S⁻(0) = 0, rather than Karlin’s -1, so the rank-zero/null cases must be translated explicitly.

Required source proof route

1. Introduce Mathlib-shaped predicates for common weak/strict sign of order-r minors. These are genuine property definitions, so def ... : Prop is appropriate here; they must not be named ...Statement or used to hide an unproved theorem.
2. Formalize Proposition 1.1: the Gaussian matrix F(a)_{ij} = exp(-a (i-j)^2) is strictly totally positive and tends to the identity as a → ∞.
3. Formalize Proposition 1.2 by Cauchy–Binet: if A is SC_r and has full column rank, then F(a)A is SSC_r, and F(a)A → A.
4. Full-column-rank case: apply the already formalized V.1.1 strict maximal-minor theorem to F(a)U, then pass to S⁻(Uc) ≤ m-1 using the lower-semicontinuity/stability lemma for finite-vector sign variations under convergence.
5. Deficient-rank case: follow Karlin’s induction on the number of columns. From a contradiction witness with r+1 alternating nonzero output coordinates, construct the source kernel vector z; choose a column j₀ so deleting it preserves rank r; set t₀ = -c_{j₀}/z_{j₀} so c+t₀z has a zero j₀ coordinate; identify the output with the column-deleted matrix and apply either the full-rank case or the induction hypothesis.
6. Do not replace the deficient-rank argument by an unproved rank/variation assumption or an alternate theorem.

Proposed main declaration

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

The exact linear-map spelling should be adjusted to the existing Mathlib matrix API rather than introducing a project-only rank wrapper.

Acceptance criteria

• No sorry, axioms, or theorem-shaped def ...Statement : Prop.
• Full-rank approximation and deficient-rank induction are separate reusable lemmas.
• Cauchy–Binet strictification and the finite-vector sign-variation limit lemma are proved, not assumed.
• Focused and full CI are green.
• The final theorem is strong enough to feed Karlin V.1.4 and the ASW forward implication.

[PerAlexandersson]

Independent API foundation opened as draft PR #294 (4aafb1c). It defines genuine Matrix.IsSignConsistentOrder, IsStrictlySignConsistentOrder, IsSignRegular, and IsStrictlySignRegular predicates, with TNN/strict-positive-minor bridges and fixed-column projections. Isolated Axle check 08ecb583-53e0-4b04-9ae0-05dfa22e07ca is clean; repository CI is pending. No Gaussian approximation, rank-induction theorem, axiom, or theorem-shaped proposition placeholder is included yet.

[PerAlexandersson]

PR #294 now also contains the elementary structural API needed by the source induction/strictification steps: ordered-submatrix and transpose closure (9f28549, Axle a99217fb-7dea-4318-b4a4-8b5ab1d8a504), plus orientation of all order-q minors from one positive or negative reference minor (34aa2b0, Axle 14c43960-3909-4d05-8a3c-482a6a0d114e). The next work item remains analytic: Karlin Proposition 1.1 Gaussian STP and Proposition 1.2 Cauchy-Binet strictification. Those have not been assumed or claimed.

[PerAlexandersson]

PR #294 now has the CI repair at 2e279f1: only the two TNN bridge lemmas use fresh partially ordered index types, avoiding the Preorder/PartialOrder instance diamond. The declaration shape passed Axle request d58f3a98-f189-462f-828c-ece34eb8dc1a; project Comparator and Lean Action runs are in progress. This PR remains API foundation only: it does not claim Karlin V.1.3, whose next source step is still the Gaussian F(a)/Proposition 1.1 and Proposition 1.2 strictification route.

[PerAlexandersson]

Source-ordered progress pushed to draft PR #294 as f739e9a. Added Matrix.gaussianMatrix and proved its entry, diagonal, positivity, and exact atTop convergence to the identity via Matrix.tendsto_gaussianMatrix_atTop. Axle 4.31 accepted the isolated declarations (request 5f717093-30cb-4027-9188-537986ac4aac). No STP claim or theorem-shaped placeholder was introduced. The next obligation remains Karlin III.1's exponential-kernel ordered-minor positivity via the extended-determinant/Wronskian argument, followed by the Gaussian row/column factorization and only then Proposition V.1.2 Cauchy--Binet strictification. No local build/test was run.

[PerAlexandersson]

Pushed source-ordered checkpoint b2b53d3 to PR #294. It adds Matrix.exponentialKernelMatrix, the exact Gaussian-minor factorization Matrix.det_gaussianMatrix_submatrix_eq, and the documented positivity transfer Matrix.det_gaussianMatrix_submatrix_pos_of_exponentialKernel. The latter keeps Karlin III.1's exponential-kernel determinant positivity as an explicit hypothesis; it does not claim Gaussian STP. Mathlib has ordinary Vandermonde support but no generalized-Vandermonde/exponential-kernel positivity theorem, so the next source obligation is the extended-determinant/Wronskian proof for det (exp (x_i y_j)) > 0 under strictly increasing coordinates. Axle 4.31 request cd6dcf63-a057-482c-93b8-df7574a0c030 accepted the isolated declarations without warnings. No local build/test was run.

[PerAlexandersson]

Scheduled cleanup checkpoint pushed as on PR #294. now uses direct Mathlib determinant/tactic imports instead of an unused project-level dependency, and is generalized from square indices to arbitrary row/column index types. Existing determinant applications retain the same specialization. Axle 4.31 checked the narrowed imports and generalized declaration (requests , ). A broader read-only audit is being persisted locally in . No local build/test was run.

[PerAlexandersson]

Correction to the preceding cleanup comment: scheduled cleanup checkpoint 1a64910 is on PR #294. Gaussian.lean now uses direct Mathlib determinant/tactic imports instead of an unused project-level SignRegular dependency, and Matrix.exponentialKernelMatrix is generalized from square Fin q indices to arbitrary row/column index types. Existing determinant applications retain the same specialization. Axle 4.31 checked the narrowed imports and generalized declaration in requests 73f2686d-7f51-47d0-bd3e-13c62c2ee52d and f08c63e5-06d5-47d9-80e7-7477b7455ec3. A broader read-only audit is being persisted locally in PR294_CLEANUP_PLAN.md. No local build/test was run.

[PerAlexandersson]

Pushed source-ordered checkpoint adeb8ca to PR #294. Added generic Matrix.det_vandermonde_pos_of_strictMono, exponential-kernel translation determinant identities, and the actual iterated-derivative Wronskian API Matrix.exponentialWronskianMatrix. Theorems Matrix.det_exponentialWronskianMatrix_eq and Matrix.det_exponentialWronskianMatrix_pos now prove Karlin's exponential Wronskian is a positive exponential product times a positive Vandermonde determinant. The remaining III.1 obligation is precisely the extended-determinant transfer from the required positive Wronskians to a positive ordered evaluation determinant; no Gaussian STP conclusion or placeholder was assumed. Axle 4.31 checked the component declarations without warnings. No local build/test was run.

[PerAlexandersson]

Proof run 2 adds the generic algebraic reduction used in Karlin's extended-determinant argument:

• Matrix.det_eq_det_adjacentRowDiff_of_firstColumn_eq_one
• subtracts each row from its successor via det_eq_of_forall_row_eq_smul_add_pred
• expands along the resulting first column to expose the smaller adjacent-difference determinant

This follows the source proof route for exponential-kernel strict total positivity; it is not a replacement route inferred from the target statement.

Axle accepted the isolated theorem under Lean 4.24.0 with no errors or warnings (request 05367106-85c6-4992-8a3f-719c3364c9c4). No local Lake build was run in this pass.

Next source obligation: write adjacent exponential differences as interval integrals, then pass determinant multilinearity through the rowwise integrals/Fubini so induction supplies a positive integrand.

[PerAlexandersson]

Proof run 1 after the cleanup cycle adds Karlin's next source-derived identity:

• new upstream-shaped shim RealRooted/Mathlib/Analysis/SpecialFunctions/ExpIntegral.lean
• theorem Real.intervalIntegral_mul_exp_mul
• formalizes
  integral t in a..b, z * exp (t * z) = exp (b * z) - exp (a * z)

This is precisely the fundamental-theorem-of-calculus step converting every adjacent exponential row difference into an interval integral. The Gaussian module now imports the shim.

Axle accepted the theorem with narrow owning imports and no Lean errors or warnings (request e475ff41-33d0-425d-9fdf-4e16bf1603b4). No local Lake build was run.

The next source obligation is unchanged: move the finite determinant through the rowwise interval integrals/Fubini, after which the induction hypothesis supplies positivity of the smaller exponential-kernel determinant.

[PerAlexandersson]

Proof run 2 adds the next source-derived multilinearity step:

• new shim RealRooted/Mathlib/LinearAlgebra/Matrix/Determinant/Integral.lean
• theorem Matrix.det_updateRow_intervalIntegral
• packages determinant linearity in one fixed row as a private finite-dimensional linear map
• uses ContinuousLinearMap.intervalIntegral_comp_comm to commute that row with an interval integral

Iterating this theorem is the finite determinant/Fubini passage in Karlin's extended-determinant proof. It does not assert positivity or replace the source argument.

Axle accepted the theorem with narrow imports and no Lean errors or warnings (request 9b6be390-cb31-4cc1-83d3-b68a69e4056c). No local Lake build was run.

Next obligation: specialize to rows z_j * exp (t * z_j), iterate the one-row theorem, and derive strict positivity of the ordered-box integral from the smaller exponential-kernel determinant and positive column factors.

[PerAlexandersson]

Proof run 1 adds the pointwise source bridge

Matrix.exponentialKernelMatrix_succ_sub_castSucc_eq_intervalIntegral.

It identifies every adjacent exponential-kernel row difference with the interval integral of
y_j * exp (t * y_j) over the corresponding consecutive x interval. This is exactly the entrywise identity used before Karlin applies determinant multilinearity.

Axle accepted the theorem with no errors or warnings (request ab4f0241-9720-49ef-8e79-42430ab4dced). No local Lake build was run.

Mathlib already provides intervalIntegral.integral_pos, with the continuity, nonnegativity, and positive-witness hypotheses needed for strict positivity, so no duplicate wrapper was introduced.

Next: iterate Matrix.det_updateRow_intervalIntegral over all rows and discharge those positivity hypotheses from strict coordinate order and the smaller exponential-kernel determinant.

[PerAlexandersson]

Proof run 2 adds the generic finite determinant/Fubini bridge:

Matrix.det_integral_rows_eq_integral_det.

The theorem states that a determinant whose rows are coordinatewise integrals equals the product-measure integral of the pointwise determinant. Its proof follows Karlin's source mechanism:

1. expand the transposed determinant by permutations;
2. apply MeasureTheory.integral_fintype_prod_eq_prod to each row-product;
3. commute the finite permutation sum with the integral;
4. reassemble the pointwise determinant.

The statement is generic over a finite row type, a measurable coordinate space, and row-indexed sigma-finite measures, with explicit coordinate integrability.

Axle accepted the broad-import proof (5678d39a-ac00-4c9c-9b26-559678bf6fbc) and final narrow-import version (ac0aac14-2cb8-494a-8dec-12eb75d79f6f) without Lean errors or warnings. No local Lake build was run.

Remaining source step: use restricted-volume measures on consecutive x intervals, factor the positive shifted y columns, and prove strict positivity of the product-measure integral from the induction hypothesis on the interior ordered box.

[PerAlexandersson]

Proof run 1 adds the remaining generic product-measure convenience lemma:

Matrix.integrable_det_pi.

It proves integrability of the pointwise determinant under a finite product measure from integrability of every row-coordinate entry. The proof uses:

• Matrix.det_apply_row;
• MeasureTheory.Integrable.fintype_prod;
• finite-sum integrability;
• the real normalization of permutation signs.

This is the exact prerequisite identified by the Karlin III.1/V.1 API audit before applying strict integral positivity to the restricted consecutive-interval box.

Axle accepted the theorem without errors or warnings (request 7386efd7-6335-4c01-a12b-44f5ce2cdb60). No local Lake build was run.

Next: set each row measure to volume restricted to Ioc (x i.castSucc) (x i.succ), prove exponential derivative entry integrability, and derive strict positivity of the determinant integrand from the induction hypothesis.