The enumeration table of rectangular weighing designs W(m, z)k: the starred cells settled exactly, and four printed values corrected
Abstract
A weighing design W(m, z)k in the sense of Lejeune Herman and Goos (arXiv:2608.04814) is an m × z matrix over {0, ± 1} with exactly k non-zero entries in every column, at most m-k zeros in every row, and W^(T)W=kI_z. Their Table 1 counts the isomorphism classes (row and column permutations, row and column sign changes) for 4 ≤ m ≤ 24 with two zeros per column when m is even and three when m is odd; the entries marked star were obtained by a partial enumeration and are lower bounds. We re-enumerate the whole table by canonical augmentation with a canonical form in place of the pairwise isomorphism tests of the source, at a total cost of 2.8 processor-hours against the 9.6 days the source reports for one extension step. Of the 111 completely enumerated cells, 106 reproduce exactly. The other five are corrections: the cell cell53 holds one class, not three; the m=23 row is 5,22,119 at z=3,4,5, not 2,4,59, and it does not terminate at z=5 but continues with 459 and 1834 classes at z=6,7; and cell(24, 4) holds 77 classes, not 72. All 25 starred cells of the rows m=16 and m=18 and of the cells z ≤ 7 (m=20), z ≤ 6 (m=22), z=5 (m=24) are settled exactly; every exact value exceeds the printed bound, by a factor of up to 1806, and the m=18 row runs four columns further than the table prints. Two of the exact values — at the square cells cell(16, 16) and, past the printed row, cell(18, 18), which are the classical W(16,14) and W(18,16) — agree with counts announced by Lampio and Ganzhinov in 2025 and are replications; for the rest we found no prior enumeration. For 26 cells a refuting statement is verified in Lean 4: an explicit list of designs, each checked against the definition, pairwise separated by a proved isomorphism invariant, and longer than the printed entry — at cell(23)6 and cell(23)7, where the table prints nothing, the list refutes the termination mark instead; at cell53 the exhaustive half is verified as well.
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-09-07 03:53 UTC
File fingerprint
50489fd617d164b2301e02754489e19a58311f3dcf310f139bfa1376ef8a29bb
Claim ledger
Stated results
WD1routine2026-09-07
The object IsWD m z k (columns of weight k, rows carrying at most m-k zeros, W^T W = k I_z), the isomorphism relation Iso z generated by row permutations, row sign flips and column moves, and two isomorphism invariants invKey / invKey2 with invKeyₒfᵢso, pairwiseₙotᵢso and the packaged certificate lower_boundₒf_cert; five negative controls
WD2correction2026-09-07
Table 1 of arXiv:2608.04814v1 understates its own m = 23 row: there are at least 5, 22 and 111 pairwise non-isomorphic weighing designs W(23,z,20) at z = 3, 4, 5, where the table prints 2, 4 and 59; the exact counts are 5, 22 and 119
WD3correction2026-09-07
The double-dagger at cell (m,z) = (23,5) of Table 1 – 'there are no more valid zero-pattern extensions allowing a larger design' – is false: weighing designs W(23,6,20) and W(23,7,20) exist, at least five pairwise non-isomorphic of each; the exact counts are 459 and 1834, and the row terminates at z = 8
WD4candidate2026-09-07
Table 1 cell (20,5), printed 603 with a star (partial enumeration): at least 604 pairwise non-isomorphic weighing designs W(20,5,18); the exact count is 2071
WD5candidate2026-09-07
Table 1 cell (16,7), printed 2210 with a star: at least 2211 pairwise non-isomorphic weighing designs W(16,7,14); the exact count is 8165
WD6candidate2026-09-07
Table 1 cell (18,6), printed 3112 with a star: at least 3113 pairwise non-isomorphic weighing designs W(18,6,16); the exact count is 21923
WD7candidate2026-09-07
Table 1 cells (18,13) and (18,14), printed 80 and 18 with stars: at least 81 and 19 pairwise non-isomorphic designs; the exact counts are 2162 and 794, and the m = 18 row does not stop at z = 14 – it runs to z = 18 with counts 184, 52, 4, 4 and is empty at z = 19
WD8candidate2026-09-07
Table 1 cell (22,5), printed 2301 with a star: at least 2302 pairwise non-isomorphic weighing designs W(22,5,20); the exact count is 4248
WD9correction2026-09-07
Table 1 cell (5,3) prints 3; the number of isomorphism classes of weighing designs W(5,3,2) is exactly 1 – every such design is isomorphic to one explicit W0, with the exhaustive half kernel-checked over all 40³ labelled candidates
WD10correction2026-09-07
Table 1 cell (24,4) prints 72; there are at least 77 pairwise non-isomorphic weighing designs W(24,4,22), and the exact count is 77
WD11candidate2026-09-07
Table 1 cell (24,5), printed 488 with a star: at least 489 pairwise non-isomorphic weighing designs W(24,5,22); the exact count is 7857
WD12candidate2026-09-07
Table 1 cells (20,6) and (20,7), printed 5694 and 2236 with stars: at least 5695 and 2237 pairwise non-isomorphic designs; the exact counts are 167231 and 4038672
WD13candidate2026-09-07
Table 1 cell (22,6), printed 8510 with a star: at least 8511 pairwise non-isomorphic weighing designs W(22,6,20); the exact count is 909508
WD14measurement2026-09-07
The cost of isomorph rejection in this enumeration: replacing the source's pairwise graph-isomorphism filter by a canonical form turns its 9.6-day m = 16, z = 5 -> 6 step into 1.3 s and its whole m = 16 row into 24 s, at 26-30 microseconds per nauty call on the 2m + 2z <= 88 vertex graphs that arise; and, in Lean, shipping a design list as a chain of ++-joined 120-character chunks blows maxRecDepth past about 1 MB of data and is slower and hungrier below it (45 s / 7.13 GB against 16 s / 6.98 GB on the same 248 kB of data), so ship one string literal however long
This ledger entry is reported in prose and is not bound to a Lean theorem.WD15known data2026-09-07
Independent replication of Table 1's completely-enumerated cells: 19 of its 21 complete rows reproduce exactly, cell for cell (m = 4, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 24 as far as each was printed complete), and every dagger / double-dagger termination claim holds except the one at (23,5)
This ledger entry is reported in prose and is not bound to a Lean theorem.WD16candidate2026-09-07
Table 1 cells (18,7) through (18,12), printed 3375, 1157, 375, 793, 597 and 318 with stars: at least 3376, 1158, 376, 794, 598 and 319 pairwise non-isomorphic designs; the exact counts are 114374, 114178, 48044, 25613, 12376 and 5838
WD17candidate2026-09-07
Table 1 cells (16,8), (16,9) and (16,10), printed 1889, 1049 and 821 with stars: at least 1890, 1050 and 822 pairwise non-isomorphic designs; the exact counts are 9931, 8158 and 6316
WD18candidate2026-09-07
The exact counts at the six cells of Table 1 that the isomorphism invariant of this family cannot separate: (16,11) = 3404, (16,12) = 1729, (16,13) = 519, (16,14) = 202, (16,15) = 30, (16,16) = 17, against the printed 472, 396, 147, 67, 11 and 7; the m = 16 row is empty at z = 17
This ledger entry is reported in prose and is not bound to a Lean theorem.Provenance
- Generated by
- Machina Mathematica
- Released by
- Korea Superintelligence Labs
- Source context
- A weighing design W(m, z, k) is, in the sense of arXiv:2608.04814v1 §2 (verbatim), "a matrix of size m × z with entries from 0, ±1, in which each column contains exactly k non-zero entries and each row contains at most m − k zeros"; its columns are mutually orthogonal, WᵀW = k I_z. It is the non-square generalisation of a weighing matrix W(m, k) (z = m, k = m − 1 a conference matrix, k = m a Hadamard matrix). The row bound is part of the definition and is easy to miss: without it the counts are different objects.
- Snapshot
- 2026-09-07 03:53 UTC
- Ledger commit
801848d7