9.5 Exact finite enumeration
On this page · Permalink · Source line 1621
This section describes the computer-assisted part of the paper. The computations use integer encodings only. No floating-point decisions occur.
9.5.1 Restricted breadth-first search
On this page · Permalink · Source line 1625
Over \({\mathbb F}_2\), an element of \({\operatorname{U}}_n({\mathbb F}_2)\) is determined by its \(n(n-1)/2\) strict lower entries. For \(n=6\) there are \(2^{15}=32768\) states. Breadth-first search from the identity using the fifteen lower transvections gives every restricted distance and the restricted diameter.
For \(n=6\), the restricted diameter is eight. Therefore every lower-unitriangular target has ambient distance at most eight. This makes a radius-four meet-in-the-middle search complete.
9.5.2 Ambient radius-four ball and right-coset pairing
On this page · Permalink · Source line 1631
Let
Exact breadth-first search gives
Group \(B_4\) by right cosets of \({\operatorname{U}}_6({\mathbb F}_2)\). If \(a,b\) lie in the same right coset, then
and
The implementation uses a canonical right-coset key obtained by reducing matrix columns from right to left. Right multiplication by a lower-unitriangular matrix changes column \(j\) only by a combination of columns with larger index, so this reduction is constant on right cosets and separates them.
Lemma 9.28: Meet-in-the-middle completeness
For every \(u\in{\operatorname{U}}_6({\mathbb F}_2)\),
Proof
Every pair on the right gives a word for \(u\), so the right-hand side is at least \({\ell_{*}}(u)\). Conversely, \({\ell_{*}}(u)\le8\). Take a shortest path from the identity to \(u\) and split it at a midpoint. The prefix endpoint \(a\) has distance at most four. The inverse of the remaining suffix is an element \(b\) of distance at most four, and \(u=b^{-1}a\). Hence the minimum is at most \({\ell_{*}}(u)\).
The radius-four ball splits into \(6948\) right-coset buckets. The largest bucket has \(3775\) elements. The computation checks \(45178326\) ordered pairs and recovers an ambient distance for every one of the \(32768\) targets.
9.5.3 The exact binary census
On this page · Permalink · Source line 1666
| \({\ell_{\downarrow}}\) | \({\ell_{*}}\) | number of targets |
|---|---|---|
| 0 | 0 | 1 |
| 1 | 1 | 15 |
| 2 | 2 | 125 |
| 3 | 3 | 720 |
| 4 | 4 | 2914 |
| 5 | 5 | 7851 |
| 6 | 6 | 12656 |
| 7 | 6 | 20 |
| 7 | 7 | 7926 |
| 8 | 8 | 540 |
Proof of Theorem 9.2
For \(n=2,3,4,5\), complete restricted breadth-first search and complete ambient meet-in-the-middle search return zero defects. The state counts are respectively \(2,8,64,1024\). For \(n=6\), Lemma 9.28 proves that the ambient calculation is exhaustive. The resulting distribution is Table 9.1; its counts sum to \(32768\), no target is missing, and the only strict pair is \((7,6)\) with multiplicity twenty.
Proof of Theorem 9.3
The analytic generator of Proposition 9.27 produces twenty distinct targets without reference to the distance census. Exact set comparison shows that these twenty targets are precisely the twenty off-diagonal targets in Table 9.1. Each therefore has distances \((7,6)\), and no other dimension-six target is defective.
9.5.4 Ternary and additional field checks
On this page · Permalink · Source line 1705
For \({\mathbb F}_3\), every nonzero scaled transvection is included. Complete searches give the data in Table 9.2.
| field | \(n\) | \(|{\operatorname{U}}_n({\mathbb F})|\) | restricted diameter |
|---|---|---|---|
| \({\mathbb F}_2\) | 2 | 2 | 1 |
| \({\mathbb F}_2\) | 3 | 8 | 2 |
| \({\mathbb F}_2\) | 4 | 64 | 4 |
| \({\mathbb F}_2\) | 5 | 1024 | 6 |
| \({\mathbb F}_3\) | 2 | 3 | 1 |
| \({\mathbb F}_3\) | 3 | 27 | 3 |
| \({\mathbb F}_3\) | 4 | 729 | 5 |
| \({\mathbb F}_3\) | 5 | 59049 | 7 |
The \(n=5\) ternary computation uses radius-three and radius-four balls, checks \(38415205\) right-coset pairs, and recovers all \(59049\) targets. It finds no defect. The field-independent Theorem 9.1 supplies a defect at \(n=6\), proving Theorem 9.4. Separate exact searches over \({\mathbb F}_3\) and \({\mathbb F}_5\) verify the distances of the canonical atom directly. The \({\mathbb F}_5\) calculation is an audit of the atom, not a complete threshold computation below dimension six.
9.5.5 Verification status
On this page · Permalink · Source line 1732
The analytic proofs of Theorem 9.1 and Corollary 9.52 do not depend on computation. The claims in Theorem 9.2, Theorem 9.3, and Theorem 9.4 depend on exact finite enumeration. The source archive contains:
the C++ programs for every breadth-first and meet-in-the-middle search;
the Python program that independently generates the twenty motifs and compares sets;
symbolic checks for the bounded-resource formulas and the totally unimodular \(M(K_4)\) representation;
exact stdout files and JSON packet data;
SHA-256 checksums;
build and reproduction commands.
The programs were rebuilt from source and rerun independently when this manuscript was assembled; the outputs matched byte for byte.