The column number s(Delta, r) of Delta-modular matrices (Problem 1.1 of arXiv:2509.13463)

Heller 1957: s(1,r) >= C(r+1,2) at r = 2, 3, 4, from [Iᵣ | Dᵣ], stated with Matrix.det

Lee-Paat-Stallknecht-Xu A(Delta,r): s(Delta,r) >= C(r+1,2) + (Delta-1)(r-1) for Delta = 2,3,4,5 and r = 3,4

Paat-Walsh-Xu A(Delta,lambda,r): one extremal matrix per partition lambda of Delta-1, nine partitions at r = 4

s(3,3) >= 11 from the paper's own sporadic rank-3 matrix, one column above its large-r formula 10; and that matrix is maximal among identity-normalised extensions

s(2,3) >= 9, the exceptional Lee et al. value, from a witness found here by exhaustion; also maximal

Averkov-Schymura's counterexamples rebuilt from their construction: c(4,3) >= 16 > 15, c(4,4) >= 24 > 22, c(8,4) >= 40 > 38

The same counterexamples in the pairwise-non-parallel count: s(4,3) >= 13 and s(9,4) >= 37, both BELOW the conjectured bound – the refutations are of the c form only

Lee et al.'s conjecture FAILS at Delta = 9: an explicit rank-4 integer matrix with 43 columns, none zero and no two equal up to sign, all 4 x 4 minors at most 9 in absolute value, against the conjectured 42

c(8,4) >= 39 from a PLANAR base set, where Averkov-Schymura used a three-dimensional one

Negative controls for the family

Infrastructure that makes the rows above mean what they say: detRows IS Matrix.det at r = 2,3,4; subseqsLen IS List.sublistsLen; parallel columns have vanishing 2 x 2 minors

detRows is Matrix.det at every rank, by one induction: the recursive argument of detRows is the Matrix.submatrix of Matrix.detₛuccᵣow_zero, because deleting a list entry is Fin.succAbove

the four rank-5 rows the 2026-08-23 landing left at the Facts level, promoted to Matrix.det: s(1,5) ≥ 15, s(2,5) ≥ 19, s(3,5) ≥ 23 twice

s(2,5) ≥ 20 and c(2,5) ≥ 20: the second exceptional value of arXiv:2509.13463 §1, witnessed by the matrix Lee et al. print, in both of their descriptions

negative controls for the rank-5 layer: a too-large modularity claim refuted through Matrix.det, the rank hypothesis non-vacuous at rank 5, a parallel column and its negation rejected while the matrix stays Δ-modular, the one column the c form allows shown to break modularity, and a too-small claim refuted

⟨crossVec n T, c⟩ = det [T | c] at every rank, by Laplace expansion along the last column; plus the three Prop ↔ Bool directions maximality needs (parallelVₒfₚarallelB, maxAbsMinorₗeₒfᵢsDeltaModular, noExtₒfₑxtFast / noExtₒfₑxtensions)

s(3,4) ≥ 17, one above C(5,2) + 2·3 = 16: rank 4 is a second sporadic rank for Δ = 3, beyond the rank-3 matrix arXiv:2509.13463 displays

s(3,5) ≥ 25, two above C(6,2) + 2·4 = 23: rank 5 is a third sporadic rank for Δ = 3

s(4,4) ≥ 22 — Paat–Walsh–Xu's own extremal matrix A(4,(1,1,1),4) is not maximal: it absorbs e₂−e₃−e₄, e₂−e₃+e₄, e₂+e₃−e₄. Also A(4,(2,1),4) absorbs one column, and the other seven rank-4 partition matrices do not

s(5,4) ≥ 24, two above C(5,2) + 4·3 = 22 — the other value arXiv:2509.13463 §1 says its method could reach "with the help of computing"

Maximality of five witnesses among identity-normalised extensions, stated about Matrix.det — including extensions 2 5 lpsxExc25 = [], the item journal/2026-08-23-column-number-provenance.md §6 priced and parked

The three Bool maximality facts Facts.lean has carried since the landing — sporadicₘaximal, exc23ₘaximal, hellerₜhreeₘaximal — promoted from statements about the private maxAbsMinor to statements about Matrix.det

Negative controls for the new layer