Add sign-regular matrix predicate API - #294

Merged

PerAlexandersson merged 141 commits into

mainfrom

codex-karlin-v13-api

Aug 5, 2026

Commits on Aug 2, 2026

Add sign-regular matrix predicates
PerAlexandersson
committed
6ca9391
Add sign-regular closure lemmas
PerAlexandersson
committed
5a65f49
Orient sign-consistent minors
PerAlexandersson
committed
4803470
Scope sign-regular index orders
PerAlexandersson
committed
d80295e
Add Karlin Gaussian identity limit
PerAlexandersson
committed
9e310e6
Factor Karlin Gaussian minors
PerAlexandersson
committed
97a97eb
Generalize exponential kernel matrix
PerAlexandersson
committed
685adf5
Prove exponential Wronskian positivity
PerAlexandersson
committed
ab5ee59
Add adjacent-row determinant reduction
PerAlexandersson
committed
bace71e
Deduplicate transpose minor proofs
PerAlexandersson
committed
bd2b50b
Add exponential difference integral identity
PerAlexandersson
committed
5a81d7d
Commute one determinant row with interval integrals
PerAlexandersson
committed
81c45c3
Deduplicate Gaussian determinant imports
PerAlexandersson
committed
4c63332
Bridge exponential row differences to integrals
PerAlexandersson
committed
1ce350e
Integrate determinants over row products
PerAlexandersson
committed
6efed9b
Deduplicate row determinant expansions
PerAlexandersson
committed
86dcb14
Prove product determinant integrability
PerAlexandersson
committed
38d1156
Specialize determinant integrals to adjacent intervals
PerAlexandersson
committed
5178408
Clarify row determinant integrability name
PerAlexandersson
committed
0757284
Prove adjacent exponential determinant positivity
PerAlexandersson
committed
1490ce9
Prove exponential kernel strict positivity
PerAlexandersson
committed
368d7df
Golf ordered-box monotonicity proof
PerAlexandersson
committed
5c10332
Prove Gaussian strict minor positivity
PerAlexandersson
committed
c71d27d
Simplify Gaussian minor monotonicity proof
PerAlexandersson
committed
3e0370e
Add rectangular determinant expansion
PerAlexandersson
committed
2338090
Reassemble rectangular determinant expansion
PerAlexandersson
committed
8fe98b9
Generalize noninjective submatrix determinant lemma
PerAlexandersson
committed
28beaa6
Factor injective maps through ordered images
PerAlexandersson
committed
5e0ad90
Prove uniqueness of ordered image factorization
PerAlexandersson
committed
87f2110
Deduplicate ordered image range proof
PerAlexandersson
committed
ae50ccb
Reindex embedding sums by ordered images
PerAlexandersson
committed
2d846d2
Prove selected-minor Cauchy-Binet identity
PerAlexandersson
committed
fecbbec
Deduplicate Cauchy-Binet sum proof
PerAlexandersson
committed
ce4ec90
Extract ordered nonzero minor from full rank
PerAlexandersson
committed
e93697f
Formalize Karlin Gaussian strictification
PerAlexandersson
committed
b7765b5
Reuse matrix multiplication continuity
PerAlexandersson
committed
b0adb9e
Prove lower semicontinuity of sign variations
PerAlexandersson
committed
d6819a7
Prove full-rank sign variation bound
PerAlexandersson
committed
b99e0e5
Golf sign variation limit proofs
PerAlexandersson
committed
845e161
Preserve alternating rows under kernel perturbation
PerAlexandersson
committed
99bdbb6
Extract ordered nonzero rank minors
PerAlexandersson
committed
9c22309

Commits on Aug 3, 2026

Golf rank minor independence proof
PerAlexandersson
committed
3c419fb
Preserve rank after deleting an avoided column
PerAlexandersson
committed
0333da3
Prove the signed row-cofactor kernel identity
PerAlexandersson
committed
a640e3e
Golf signed cofactor kernel proof
PerAlexandersson
committed
4e28245
Compose Karlin's nonzero-cofactor branch
PerAlexandersson
committed
729561e
Reassemble deleted-column matrix products
PerAlexandersson
committed
927ec43
Golf coefficient cancellation proofs
PerAlexandersson
committed
4a407ca
Prove Karlin cofactor branch contradiction
PerAlexandersson
committed
355e53d
Construct Karlin supported column relation
PerAlexandersson
committed
dc345f3
Golf Karlin supported relation proofs
PerAlexandersson
committed
9865b3c
Add Karlin rank deletion induction adapter
PerAlexandersson
committed
10db3a1
Prove Karlin deficient-rank induction step
PerAlexandersson
committed
e84bbbb
Golf Karlin rank induction adapters
PerAlexandersson
committed
df0924c
Prove Karlin rank-sensitive variation bound
PerAlexandersson
committed
317b01f
Preserve sign consistency under TN right products
PerAlexandersson
committed
6ad9dba
Deduplicate Karlin rank-zero induction case
PerAlexandersson
committed
8b862f6
Prove monotone incidence minor formula
PerAlexandersson
committed
2995115
Show monotone incidence matrices are TN
PerAlexandersson
committed
a2a4c8f
Define weighted incidence aggregation
PerAlexandersson
committed
57d595e
Deduplicate weighted incidence matrices
PerAlexandersson
committed
4808221
Reconstruct weighted block coefficients
PerAlexandersson
committed
abdc80d
Preserve signs under weighted aggregation
PerAlexandersson
committed
801a081
Extract weighted incidence mulVec formula
PerAlexandersson
committed
d9bdef5
Assemble Karlin bound from sign blocks
PerAlexandersson
committed
ee10258
Define prefix sign variations
PerAlexandersson
committed
1e3662b
Move sign block API to sign variation
PerAlexandersson
committed
a83fa4a
Prove prefix sign variation monotonicity
PerAlexandersson
committed
81ae5d5
Define monotone sign block indices
PerAlexandersson
committed
4901e7f
Bound adjacent prefix sign variations
PerAlexandersson
committed
d17a5a5
Add sign block index simp lemmas
PerAlexandersson
committed
3651965
Preserve prefixes under destuttering
PerAlexandersson
committed
d4df0a6
Preserve final element under destuttering
PerAlexandersson
committed
03b3cff
Prove constant sign on sign-block fibers
PerAlexandersson
committed
57ef0da
Clean up sign-block proof and repair clean builds
PerAlexandersson
committed
e9aed1a
Construct the finite sign-block decomposition
PerAlexandersson
committed
6bb98e7
Derive sign-regular variation diminution
PerAlexandersson
committed
05974d2
Golf finite sign-block reconstruction
PerAlexandersson
committed
5a46e8a
Derive rectangular TN variation diminution
PerAlexandersson
committed
ab13859
Preserve nonzero signs under finite convergence
PerAlexandersson
committed
46dd182
Reuse finite convergence sign stability
PerAlexandersson
committed
0b97f76
Prove nodal sign insertion invariance
PerAlexandersson
committed
9440b6b
Bound endpoint sign variation cost
PerAlexandersson
committed
c19d3f6
Golf endpoint variation proofs
PerAlexandersson
committed
852b2b0
Compose repeated nodal sign insertions
PerAlexandersson
committed
246cbc9
Bound complete nodal perturbation variation
PerAlexandersson
committed
9d69762
Clean up nodal endpoint composition
PerAlexandersson
committed
497a081
Preserve nodal insertions under context
PerAlexandersson
committed
48600c8
Derive opposite signs from strict nodality
PerAlexandersson
committed
cab1d03
Relate succAbove to list erasure
PerAlexandersson
committed
1ee508e
Clean up nodal bridge APIs
PerAlexandersson
committed
88cbc81
Split finite lists into endpoints and interior
PerAlexandersson
committed
13075c9
Transport neighbor triples through succAbove
PerAlexandersson
committed
63ba514
Golf succAbove triple arithmetic
PerAlexandersson
committed
2459182
Rule out the nodal deletion splice
PerAlexandersson
committed
fbbb8f9
Handle the second nodal deletion adjacency
PerAlexandersson
committed
aed2ae7
Deduplicate nodal splice contradictions
PerAlexandersson
committed
1adbaaa
Transport nodality through coordinate deletion
PerAlexandersson
committed
dd1caa6
Normalize finite sign variation lists
PerAlexandersson
committed
39a40de
Simplify sign filtering normalization
PerAlexandersson
committed
bfb0d95
Export finite indexing shims
PerAlexandersson
committed
57f1497
Relate interior coordinate deletion
PerAlexandersson
committed
446b2d9
Relate interior list deletion
PerAlexandersson
committed
62868e7
Golf interior deletion extensionality
PerAlexandersson
committed
2d5f680
Reinsert erased nodal signs
PerAlexandersson
committed
50efbae
Preserve filters when erasing rejected entries
PerAlexandersson
committed
ba7ee77
Golf filtered erasure proof
PerAlexandersson
committed
48c3d23
Define finite nodal perturbation core
PerAlexandersson
committed
774e371
Move erasure through list context
PerAlexandersson
committed
a37334b
Clean up list shim namespaces
PerAlexandersson
committed
e364e7a
Reinsert nodal signs inside list context
PerAlexandersson
committed
3183bd5
Handle endpoint nodal sign insertions
PerAlexandersson
committed
fc67c4d
Simplify endpoint nodal insertion proofs
PerAlexandersson
committed
a462dfb
prove nodal sign removal induction step
PerAlexandersson
committed
85cf74c
relocate nodal removal proof to owning module
PerAlexandersson
committed
3ceaa41
complete finite nodal insertion chain
PerAlexandersson
committed
7a46738
clean nodal induction and repair inference
PerAlexandersson
committed
d07d256
prove finite nodal perturbation bound
PerAlexandersson
committed
9a0bc95
add nodal perturbation topology wrapper
PerAlexandersson
committed
6acb195
golf nodal perturbation topology wrapper
PerAlexandersson
committed
9815323
add surjective TN nodal kernel bound
PerAlexandersson
committed
68305d4
add repeated ASW sine variation lower bound
PerAlexandersson
committed
1aa62a7
clean repeated ASW variation proof
PerAlexandersson
committed
d699e13
add sampled sine floor variation bound
PerAlexandersson
committed
f572930
prove ASW sector bound by repeated blocks
PerAlexandersson
committed
2805f67
clean repeated block sector proof
PerAlexandersson
committed
35d1c84
Remove admitted ASW backend dependency
PerAlexandersson
committed
cf22378
Fix Fin order elaboration on Lean 4.31
PerAlexandersson
committed
e4aa950
Define finite sign variations before use
PerAlexandersson
committed
8ad9e92
Remove unused sign variation simp input
PerAlexandersson
committed
1e25bb7
Add unconditional PF polynomial constructors
PerAlexandersson
committed
5cccf52
Add argument-free ASW downstream wrappers
PerAlexandersson
committed
98e0e60
Golf filtered sign variation bridge
PerAlexandersson
committed
64787cd
Add unconditional ASW pair bridge endpoints
PerAlexandersson
committed
377fe06
fix: close sign-variation bounds directly
PerAlexandersson
committed
32c134b
fix: handle truncated sign-variation counts
PerAlexandersson
committed
461659d
Fix sign variation helper normalization
PerAlexandersson
committed
c25e454
Fix rank-deficient theorem doc placement
PerAlexandersson
committed
c29af69
Avoid determinant product simp timeout
PerAlexandersson
committed
f3a38a0

Commits on Aug 5, 2026

Replace omega in sign variation proof
PerAlexandersson
committed
691e288
Clean Karlin matrix proof warnings
PerAlexandersson
committed
64426cc