Add sign-regular matrix predicate API

[PerAlexandersson]

Begins the independent API foundation for #292.

This adds genuine reusable property definitions for weak/strict common signs of order-q minors and sign regularity across all orders. It also proves the elementary bridges from rectangular TNN and strictly positive minors, plus fixed-column product projections needed by Karlin V.1.1/V.1.3.

No V.1.3 theorem, approximation fact, rank lemma, axiom, or theorem-shaped ...Statement : Prop is introduced.

The module passes isolated Axle checking with no warnings: 08ecb583-53e0-4b04-9ae0-05dfa22e07ca. Repository CI is authoritative and pending.

[PerAlexandersson]

Mandatory cleanup run 3 completed.

• Rebasing onto current main retained both the merged PR Prove Karlin strict maximal-minor variation bound #289 alternating cofactor-kernel lemma and this PR's adjacent-row determinant reduction.
• Extracted one private det_transpose_submatrix helper.
• Reused it in both weak and strict sign-consistency transpose proofs, removing two identical local proof blocks.
• Explicitly omitted the irrelevant order structures from the helper, avoiding an unused-section-variable warning.

Axle accepted the rewritten closure proofs (fcc5650a-8b87-45f4-8a5e-595dda48657b) and the warning-free helper shape (f7a3e3c1-70f7-4ec4-9152-33c536310449). No local Lake build was run.

[PerAlexandersson]

Mandatory cleanup run 3 completed with one isolated dependency deduplication.

Gaussian.lean no longer directly imports Mathlib.LinearAlgebra.Matrix.Determinant.Basic: the immediately imported project shim RealRooted.Mathlib.LinearAlgebra.Matrix.Determinant.Integral publicly re-exports that API.

This changes no declarations or proofs. No local Lake build was run. The next continuation returns to issue #292's ordered-box integral positivity step.

[PerAlexandersson]

Mandatory cleanup run 3 completed.

• Added the generic row-oriented Leibniz formula Matrix.det_apply_row.
• Refactored Matrix.det_integral_rows_eq_integral_det to normalize permutation signs once.
• Reused that local formula at both ends of the calculation.
• Removed two duplicated transpose/det_apply/unit-sign-conversion blocks.

Axle accepted the helper and refactored theorem without errors or warnings (request d7949a13-bc8b-42e8-a114-28db864286cb). No local Lake build was run.

The next continuation returns to the restricted-volume ordered-box positivity specialization for issue #292.

[PerAlexandersson]

Mandatory cleanup run 3 completed.

Renamed Matrix.integrable_det_pi to Matrix.integrable_det_rows before it acquired consumers. The new name matches PR294_INTERVAL_INTEGRAL_PLAN.md and describes the rowwise construction rather than the implementation measure.

A scoped source search found no Lean consumer to migrate. No proof changed and no local Lake build was run.

The next continuation returns to strict positivity of the restricted product integral for issue #292.

[PerAlexandersson]

Mandatory cleanup continuation 102 is pushed in commit 35d1c841.

• Updated the nonreal sector theorem documentation to describe the now-implemented repeated-matrix, nodal-perturbation, sampled-sine floor, and large-block route instead of calling classical sign-regularity a missing ingredient.
• Inlined the one-use nonnegativity witness passed to Nat.floor_le, removing three proof lines.

No theorem statement or mathematical route changed. Axle 4.31 accepted the inlined witness without warnings in request 0b67f8a8-58ff-4ae8-b542-8d37a13a7d2c. No local Lake build was run.

Continuation 103 returns to proof work on redirecting the final sector theorem through the unconditional nonreal proof.

[PerAlexandersson]

Continuation 103 removes the admitted one-block backend from the unconditional ASW route.

Commit cf223784 redirects aswKarlinSectorThreshold_le_abs_arg through the proved repeated-block nonreal theorem plus the real-root branch, and redirects aswSectorThreshold_le_abs_arg_of_isPolyaFreqSeq_coeff through that theorem. The obsolete aswKarlinKernelSignVariationClassicalInput implementation containing sorry and its unconditional convenience wrapper are deleted; the explicit _of_classicalInput compatibility API remains conditional.

Axle accepted both wrapper terms: request c75d2c03-ff97-4743-aa7e-fb58223634bb. No local Lake build was run under the current instruction; comparator CI remains the merge check.

[PerAlexandersson]

Continuation 104 repaired two concrete Lean 4.31 CI blockers and completed the issue #241 downstream audit.

• `e4aa9503`: makes the reflexive Fin-order witness explicit at the Nat level (Axle 4.31 request `9aff08d6-b531-4d8e-9cde-8786ae8c9763`).
• `8ad9e922`: moves the unchanged `Fin.signVariations` definition before its first two consumers; the prior cascading `uses sorry` warning was caused by the unknown constant, not a literal admission.

The source-faithful forward theorem is already `aissenSchoenbergWhitneyForward`, with unconditional splits/zero-aware/no-nonneg projections. A read-only audit found 44 legacy downstream declarations still accepting ASW arguments; migration order is PFPolynomial, direct SuccDegree/Hadamard consumers, PairBridge, PairwiseUpgrade, then ChudnovskySeymour. I left the tactic frontend untouched because the user-directed tactics worker owns that file. Comparator run 30792659517 is pending.

[PerAlexandersson]

Mandatory cleanup continuation 105 is pushed in commit `1e25bb71`.

The nonzero branch of `List.signVariations_append_singleton_signType_le_succ` no longer supplies `ha` to `simp`; comparator had compiled the theorem and reported that argument as unused. This is a one-line warning cleanup with no theorem statement, proof route, or normal form change.

A broader direct-`simpa only` golf for `Fin.filtered_signList_signVariations` was audited but deliberately deferred. No local Lake build was run; comparator has restarted on the pushed commit. Continuation 106 returns to proof work.

[PerAlexandersson]

Proof continuation 106 is pushed in commit `5cccf52b`.

Issue #241 now has three canonical argument-free PF entry points:

• `IsPFPolynomial.of_polyaFreqSeq`;
• `IsPFPolynomial.of_forall_pos_add_C_mul`;
• `IsPFPolynomial.splits_of_forall_pos_add_C_mul`.

They call the proved `aissenSchoenbergWhitneyForwardOrZero` theorem directly, so PF callers no longer need to supply a forward-ASW backend. Existing `of_sequence`/`_of_forward` declarations remain temporarily for compatibility because the user-directed tactics worker owns the tactic frontend. Axle 4.31 accepted the composition in request `2a562b7c-a16f-4688-a081-f59da2e1efb9`. No local Lake build was run; comparator has restarted.

[PerAlexandersson]

Proof continuation 107 is pushed in commit `98e0e600`.

Two direct issue #241 consumers now have argument-free ASW routes:

• `PosComboRealRooted.left_splits_of_asw` uses the unconditional affine-family PF splitting constructor;
• `polyaFrequencyHadamardCoeff_of_schurPolyaWagner_asw` converts both PF sequences with `IsPFPolynomial.of_polyaFreqSeq` before applying Schur--Pólya--Wagner closure.

Neither asks callers for a forward-ASW backend. Existing conditional declarations remain unchanged for compatibility, and no tactic file changed. Axle checked the wrapper shapes in requests `7bab27ac-927c-4f87-87aa-3636b1e7a65f` and `e0531301-ae01-4460-b61d-9291d80a3f52`. No local Lake build was run; comparator restarted.

[PerAlexandersson]

Mandatory cleanup continuation 108 is pushed in commit `64787cd6`.

`Fin.filtered_signList_signVariations` now composes the preceding sign-list bridge and zero-filter invariance in one direct `simpa only ... using`, replacing the separate `rw` and `exact` steps. No theorem statement, mathematical route, or compatibility API changed.

Axle 4.31 accepted the composition in request `6513e49c-0151-44e4-a625-e9c942ffd5d1`. No local Lake build was run; comparator restarted. Continuation 109 returns to issue #241 proof migration.

[PerAlexandersson]

Proof continuation 109 is pushed in commit `377fe065`.

The issue #241 migration now reaches PairBridge through three argument-free declarations:

• `PosComboSuccDegreeLeftSplitsNonnegStatement_of_asw`;
• `posComboNoCommonSuccDegreeSlotData_of_asw_and_rootCrossing`;
• `succDegreePairHasCommonInterleaver_nonneg_of_asw_and_rootCrossing`.

They instantiate the proved ASW left endpoint and reuse the existing left-splits-plus-root-crossing reductions. No caller supplies an ASW backend, while conditional APIs remain compatible. Axle 4.31 accepted the composition in request `b6adab4d-6c87-4a13-888e-6a4cfe90cf1b`. No local Lake build was run; comparator restarted.

[PerAlexandersson]

Continuation 118 pushes 32c134b6, repairing the sole current-head comparator build failure.

In both one-sign variation bounds, the destutter helper already supplied the exact required length inequality. The nonzero branches now close by simpa [List.signVariations, ha] using h instead of simplifying into a truncated-subtraction goal and invoking arithmetic automation.

Axle 4.31 checked both exact normalization shapes (request 316a934f-8eb4-4b8f-a091-ef28a2d615e6). No local Lake build was run; comparator CI is restarting. PR #295 was left untouched so its queued Lean Action can proceed.

[PerAlexandersson]

Continuation 122 pushes 461659d4, repairing the two current-head comparator errors.

The previous direct simplification missed List.signVariations' truncated subtraction. After normalization, each helper gives a <= n + 1 while the theorem target is a <= n - 1 + 1 + 1. A private two-case Nat lemma now proves that bridge, and both branches close by transitivity without lia or grind.

Axle 4.31 checked the exact arithmetic shape (request 4e2c1f3d-d15a-4180-9b52-3dd536340046). No local Lake build was run; comparator CI is restarting. PR #295 remains untouched.

[PerAlexandersson]

CI repair pushed in c25e454. Run 30795602925 exposed a normalization-only mismatch in the two one-sign variation bounds: the goal was simplified separately from the destutter helper. The repair specializes at a, splits on a = 0, and normalizes the complete using expression. Axle request 0554d65f-e0c9-4ff0-8def-6adfe393b419 checked both proof shapes.

[PerAlexandersson]

Cleanup repair pushed in c29af69f. Comparator run 30796221557 rejected open Filter Topology because it appeared between a declaration docstring and its theorem. Moving the open above the docstring restores valid command structure; the later timeout and unknown-constant diagnostics were cascades. No theorem statement or proof changed.

[PerAlexandersson]

Comparator timeout repair pushed in f3a38a0d. Run 30796780833 reached mul_of_right_isTotallyNonnegRect but timed out on the final commutative simpa over four determinant expressions. The proof now applies a private scalar cross-product lemma, checked by Axle request e32acba6-63ff-4b19-8933-da7969fb06e6. No heartbeat limit, theorem statement, or Cauchy--Binet argument changed.

[PerAlexandersson]

Comparator run 30797485835 passed on head f3a38a0. The PR is now ready for review: the exact forward ASW theorem is present, the remaining hASW parameters are compatibility APIs rather than unproved theorem content, and the final determinant-sign proof avoids the prior simp timeout. No local Lake build was used; the passing comparator is authoritative.