9.13 Search algorithms and correctness
On this page · Permalink · Source line 3136
9.13.1 Restricted search
On this page · Permalink · Source line 3138
For \({\mathbb F}_2\), each lower-unitriangular matrix is stored as a bit string. Standard breadth-first search gives exact distance because every edge has unit weight. The algorithm terminates after visiting all states.
Algorithm 9.70: Restricted breadth-first search
Initialize \(d[I]=0\) and a queue containing \(I\). Repeatedly remove \(X\) from the queue. For every lower transvection \(s\to t\), form \(Y=\tau_{t,s}(1)X\). If \(Y\) has not been visited, set \(d[Y]=d[X]+1\) and append \(Y\). Continue until the queue is empty.
9.13.2 Right-coset key
On this page · Permalink · Source line 3146
For an invertible binary matrix \(A\), let \(c_j\) be column \(j\). Starting at \(j=n-1\) and moving left, reduce \(c_j\) by the already canonicalized columns \(c_{j+1},\ldots,c_{n-1}\), using their pivot coordinates. The resulting ordered reduced columns form the key \(\kappa(A)\).
Lemma 9.71
For \(A,B\in{\operatorname{GL}}_n({\mathbb F}_2)\),
Proof
Right multiplication by \(U\in{\operatorname{U}}_n\) replaces column \(j\) by itself plus a combination of columns with index greater than \(j\). Right-to-left reduction is therefore unchanged on a right coset. Conversely, equal reduced columns imply that the original column frames differ by a unique lower-unitriangular column transformation, so \(A=BU\) for some \(U\in{\operatorname{U}}_n\).
9.13.3 Ambient search
On this page · Permalink · Source line 3163
Algorithm 9.72: Radius-four right-coset meet in the middle
Compute the exact radius-four ball \(B_4\) in \({\operatorname{GL}}_6({\mathbb F}_2)\). Bucket its elements by \(\kappa\). For each bucket and every ordered pair \((b,a)\) in that bucket, compute \(u=b^{-1}a\in{\operatorname{U}}_6\) and update
Correctness is Lemma 9.28. The computation also checks that every generated pair lies in \({\operatorname{U}}_6\) and that every one of the \(32768\) targets receives a finite distance.
9.13.4 Higher-dimensional bidirectional audits
On this page · Permalink · Source line 3175
For the targets \(H_7,H_8,H_9\) of Theorem 9.36, the program small_snapshot_exact.cpp constructs exact ambient balls from the identity and from the target. If radius-\(r\) and radius-\(s\) balls are disjoint, symmetry of the generating set rules out every word of length at most \(r+s\). The tested splits are \(3+3\), \(3+4\), and \(4+4\), respectively. The source stores matrices in one 128-bit word and uses exact row-addition transitions; no probabilistic or floating-point step occurs.
9.13.5 Symbolic higher-family checks
On this page · Permalink · Source line 3179
The program higher_family_tests.py generates the snapshot targets over \({\mathbb F}_2\), \({\mathbb F}_3\), and \({\mathbb F}_5\), evaluates both displayed circuits, computes the interval-tree potentials, audits a tensor certificate for the seven-dimensional seed, verifies the recursive cross rank, and reproduces the twenty-one-dimensional rate optimization.
9.13.6 Further generalization audits
On this page · Permalink · Source line 3183
The program further_generalization_tests.py verifies the universal circuits over \(\mathbb Z/4\mathbb Z\), \(\mathbb Z/6\mathbb Z\), and \(\mathbb Z/8\mathbb Z\), audits the rank-one bandwidth-one excursion, checks the finite-field counting bounds symbolically, and verifies the stable tensor subadditivity identities.
9.13.7 Motif comparison
On this page · Permalink · Source line 3187
The motif program independently loops over the three adjacent catalyst positions, the phase orientation, the phase leaf, and every nonempty proper before/after subset. It evaluates each six-gate word from the identity and stores its target. The resulting set has size twenty. Exact comparison with the twenty census defects returns equality.