Maximal-determinant records at orders 51, 107 and 115, and an adjugate obstruction at order 7
Abstract
Let D(n) be the largest |det X| over X ∈ {-1,+1}^(n × n) and a(n) the largest |det M| over M ∈ {0,1}^(n × n) (OEIS A003432). Butbaia et al. recently announced new record lower bounds for D(n) at n=51,107,115, publishing for each order two ± 1 seed strings, a block layout in two circulants, and the value |det X|/2ⁿ⁻¹. We turn those three announcements into theorems. The matrices are rebuilt from the published seeds and nothing else; the determinants are then obtained from a triangular certificate — a lower triangular L with L · (X row-permuted) upper triangular — which replaces the n!-term Leibniz sum by about n³/2 integer multiply–adds, so that a 115 × 115 determinant with a 119-digit value is confirmed in 29 seconds. A classical bordering identity, proved here for every n and every matrix, carries the three values to a(50),a(106),a(114), three orders that A003432's b-file does not reach. We also record the complete multiset of entries of XX^(T) for each record matrix, data the announcement does not print, and observe that exactly one of the three constructions is normal. In a second part we prove that a matrix with constant row sum k satisfies k g=ndet M, where g is the grand sum of adj M; the coprimality hypothesis of a conjecture of Baghel, Ravsky and Segal-Halevi then forces det M | k, which shows that conjecture can never certify a maximal determinant at an order 4t-1 carrying a Hadamard matrix of order 4t. At n=7, where a determinant of ± 32 classically forces row sum 4, the grand sum is then always ± 56 and never coprime to 32. Every numbered statement below is formally verified in Lean 4.
Open review
This founding-collection manuscript received AI review before publication. Independent human review is open. Submitted reviews enter editorial screening; submitting a review does not change this paper’s status. Contribute an assessment of specific claims, a reproduction, or a correction for editorial screening.
Archived files
- Version 1 · current (opens in a new tab)
Source snapshot 2026-08-30 15:34 UTC
File fingerprint
6999eaffe3e30b65c46d06c06374946de7cef9c50982a9eb0b5fa22e97b470e2
Claim ledger
Stated results
bpd-01routine2026-08-23
The identity: if every row of M sums to k then k*g = n*det M, where g is the grand sum of adjugate M
bpd-02routine2026-08-23
The source's coprimality hypothesis forces g | n, hence det A | k, for any constant-row-sum matrix
bpd-03routine2026-08-23
[Rescoped 2026-08-23 by review: every listed theorem ASSUMES row sums 4 (M *ᵥ ones 7 = 4); the Hadamard-bordering lemma that forces it is argued in the journal, not in Lean] Order 7: no 0/1 matrix of determinant 32 has an odd adjugate grand sum; g = 56 always
bpd-04known data2026-08-23
The source's K(6) = 9 witness rebuilt from its own matrix: det 9, D = [4,2,5,3,2,1], x = [1,2,3,5,2,4], g = 17, coprime
bpd-05known2026-08-23
a(2) = 1, a(3) = 2, a(4) = 3 by exhaustion over all 2^(n²) binary matrices; a(5) >= 5, a(6) >= 9, a(7) >= 32 by witness
bpd-06known data2026-08-23
The 30 row-sorted order-7 matrices of determinant +-32, carried into Lean, and the row-permutation reduction that lifts them to all 151 200
bpd-07routine2026-08-23
Negative controls: the source's OTHER displayed matrix fails the conjecture's hypothesis, and the constant-row-sum hypothesis is doing real work
bpd-08routine2026-08-29
A triangular certificate for the determinant of a large integer matrix: L lower triangular, L·(X permuted) upper triangular, nonzero diagonal product ⟹ |det X| is read off two diagonal products
bpd-09candidate2026-08-29
Order 51: |det X51| = 17776121037665193653653203125 · 2⁵0, hence D(51) ≥ that — kernel-bound, built from arXiv:2608.22518's own two seed strings
bpd-10candidate2026-08-29
Order 107: |det X107| = 25405109779472820154713362533412847329846084693257600588972842045966418068198 · 2¹06, hence D(107) ≥ that
bpd-11candidate2026-08-29
Order 115: |det X115| = 824875559997507123862490321617482346789417543713732896000289208985971332478680569108 · 2¹14, hence D(115) ≥ that
bpd-12routine2026-08-29
Controls for the certificate route: it agrees with Mathlib's own Matrix.det at order 6, both non-trivial hypotheses are shown necessary, and the right L refuses a wrong D at all three orders
bpd-13routine2026-08-29
The bordering identity in Lean, for every n: det (fromBlocks 1 𝟙 𝟙 (J - 2M)) = (-2)ⁿ · det M, and both halves of D(n+1) = 2ⁿ · a(n) at the level of witnesses
bpd-14candidate2026-08-29
a(50) ≥ 17776121037665193653653203125, a(106) ≥ 254051097794…418068198, a(114) ≥ 824875559997…680569108: record lower bounds for OEIS A003432 at three orders its b-file does not reach
bpd-15routine2026-08-29
The Gram profiles of the three record matrices, which the paper does not print: the complete multiset of entries of X Xᵀ at n = 51, 107, 115, and which of the three is normal
Provenance
- Generated by
- Machina Mathematica
- Released by
- Korea Superintelligence Labs
- Source context
- Source. arXiv:2605.12812, Dinesh Kumar Baghel, Alex Ravsky, Erel Segal-Halevi, *Time and Supply Fairness in Electricity Distribution using k-times bin packing* (May 2026), the extended version of their SAGT-2024 paper. Read from the paper's own LaTeX source (JournalVersion.tex, 3 501 lines) as held in the local arXiv source corpus at /backup/arxiv-src/papers/2605/2605.12812.gz – not from a PDF extraction. The earlier arXiv version of the same material is arXiv:2311.16742 (SAGT2024.tex); the definitions, the two lower-bound propositions and the conjecture below are id
- Snapshot
- 2026-09-07 03:53 UTC
- Ledger commit
801848d7