autSubst
plain-language theorem explainer
Literal table of how all 48 automorphisms of the 3-cube act on the five free cotree generators, written as substitution words. Separation proofs cite it as the sole trusted external datum: Lean recomputes composite tables from these words and checks them. The body is a static 48-by-5 list of integer words, not a derived construction.
Claim. A fixed list of 48 substitutions, each a 5-tuple of words in the free group on five signed generators. Entry $i$ records the images of the five generators under the $i$-th automorphism of the recognition window $Q_3$, so applying the substitution is the action of that automorphism on utterances.
background
In the Loom certificate module, an utterance is a finite list of closed walks (words) sharing a basepoint. A word is a list of integers naming the five signed cotree generators of the free group that labels walks on the recognition window.
The module stores measured search output as Lean data: a base homomorphism into $\mathrm{SL}(2,\mathbb{Z}/3\mathbb{Z})$, two witness configuration pairs, and automorphism data. The companion table of composite matrix homomorphisms is a convenience; Lean rebuilds those tables from the substitution words and checks every table by a decidable predicate, so transcription errors cannot become theorems.
What remains trusted is only provenance: that these 48 rows are exactly the generator images under $\mathrm{Aut}(Q_3)$, as measured outside Lean. Self-tests on that external configuration recover independent geometric facts (twelve oriented faces at walk length four; ninety-six Hamiltonian walks in one gauge class).
proof idea
No proof: this is a definition whose right-hand side is an explicit nested list literal. Each of the 48 outer entries is a list of five words (lists of integers). Downstream code treats membership in this list as the universe of gauge substitutions and maps each row through tableOfSubst applied to the base homomorphism when comparing against the precomputed composite tables.
why it matters
This is the trusted seed for the Loom separation theorems. Length is checked (autSubst has exactly 48 rows), and the composite tables rebuilt from these words are proved equal to the reported matrix tables, giving two independent routes to the same 48 homomorphisms.
The separation theorems then quantify over membership in this list: no gauge image of configuration A (automorphism substitution, optional global flip, basepoint move, respelling, reordering) can match B while sharing every depth-one reading; likewise for the stronger pair C and D. Those results are the kernel-checkable content of the measured certificate: identical shallow readings, distinct meanings under the full gauge group of the window.
In the broader Recognition setting the window is the eight-tick / cube geometry (T7), and these automorphisms are the discrete gauge symmetries against which semantic separation is certified.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.