autTables_eq
plain-language theorem explainer
The Python-reported composite automorphism tables agree entrywise with the tables Lean builds from the substitution words: both routes yield the same 48 homomorphisms of the recognition window. Separation arguments that quotient by the gauge action cite this equality so the enumerated automorphism list is not an opaque external artifact. The proof is a single kernel decision on finite data.
Claim. The list of composite automorphism tables equals the list obtained by mapping each automorphism substitution word through the table-of-substitution construction at the fixed base: $\mathrm{autTables} = \mathrm{map}(\mathrm{tableOfSubst}(\mathrm{base}), \mathrm{autSubst})$.
background
In the Loom separation module, two utterances A and B assert dual quantifier patterns over the open and lock relations. Shallow readings (loop-by-loop multisets, abelianised counts) are identical on the pair, so any nontrivial separation must survive the full gauge group of the recognition window: the 48 automorphisms, basepoint moves, optional reversal, respelling, and loop reordering.
autSubst is the finite list of substitution words that generate those automorphisms. tableOfSubst base turns each such word into the concrete homomorphism table relative to a fixed base. autTables is the independently reported list of composite tables (from the Python exhaustive search that chose the codebook). The module treats provenance of the automorphism action as the only external trust point; this equality closes that gap for the table representation.
The local goal is the institute-strength claim that no gauge image of one witness equals the other, with the check covering all 48 images exactly.
proof idea
One-line decidability proof: by decide. Both sides are closed finite terms (lists of tables over a finite alphabet), so Lean reduces the propositional equality in the kernel with no lemmas and no induction. The content is the agreement of the two constructions, not an algebraic rewrite.
why it matters
Without this equality, the 48-fold automorphism sweep in the separation theorems would rest on an unchecked bridge between the Python search output and the Lean substitution grammar. The module doc requires that the check cover all 48 automorphism images exactly (autSubst_length); matching tables matrix-for-matrix is the representation-level half of that coverage.
Downstream, witnesses2_separated (and the gauge non-image lemmas it uses) quantify over σ ∈ autSubst and compare gauge images of woven witnesses. Those arguments need the substitution list and the table list to name the same homomorphisms. The result is pure Loom infrastructure: it does not invoke T5–T8 or the mass ladder, but it underwrites the claim that A and B are distinct meanings rather than two spellings of one meaning under the recognition-window gauge group of order 96 times basepoint choice.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.