tableOfSubst
plain-language theorem explainer
Given a matrix table for the five free generators and a relabelling that sends each generator to a word, the composite table evaluates those words and their inverses under the original table. Anyone proving automorphism-invariance of the Loom invariant, or matching the forty-eight window automorphisms to computed tables, cites this construction. The body is a single list map over the substitution words.
Claim. For a homomorphism table $T$ that assigns to each free generator a pair of matrices $(M,M^{-1})$ in $\mathrm{SL}(2,\mathbb{Z}/3)$, and a substitution $\sigma$ sending each generator to a word $w$, the composite table is the list of pairs $(\mathrm{eval}_T(w),\mathrm{eval}_T(w^{-1}))$ ranging over the words of $\sigma$.
background
The Loom module is a certificate language for closed recognition walks on the eight-state, three-axis window fixed by the forcing chain (T7). Closed walks up to free reduction form a free group of rank five, so a finished utterance is a finite list of reduced words sharing one basepoint. Content is blind to free reduction and to simultaneous conjugation (basepoint move); the module supplies a total well-formedness checker and a computable invariant in $\mathrm{SL}(2,\mathbb{Z}/3)$ that is blind to exactly those two operations.
A table is a list of matrix pairs, one per generator: the image of the generator and the image of its inverse. A substitution (relabelling) is a list of words, one per generator, recording how an automorphism of the recognition window acts on the free generators. Word evaluation is the structural monoid homomorphism sending the empty word to the identity and a cons cell to left-multiplication by the letter matrix; word inversion reverses the walk and negates every signed letter.
The doc-comment states the intent directly: pushing a relabelling through a homomorphism yields another homomorphism, and this definition computes it, so composite tables are derived data rather than trusted input.
proof idea
Pure definition, not a proof. Map each word $g$ in the substitution list to the pair $(\mathrm{evalWord},T,g,,\mathrm{evalWord},T,(\mathrm{invWord},g))$. No lemmas are applied at the definition site; well-formedness and evaluation commutation are proved downstream.
why it matters
This is the bridge that lets the forty-eight automorphisms of the recognition window be checked by changing the table rather than rewriting every word of a configuration. Downstream, evalWord_substWord proves that reading a relabelled utterance under $T$ equals reading the original under the composite table; invariant_substConfig lifts that equality to the full Loom invariant (the relabelling half of soundness). ok_tableOfSubst shows the composite remains a valid $\mathrm{SL}(2,\mathbb{Z}/3)$ table whenever $T$ is, and matAt_tableOfSubst unpacks the $n$-th entry.
In Separation, autTables_eq identifies the Python-search composite tables with autSubst.map (tableOfSubst base), giving two independent routes to the same forty-eight homomorphisms. That agreement feeds invariant_gaugeImage and separatesEverywhere, which establish that the depth-two commutator-trace invariant separates the intended witness across the full automorphism orbit. Within the framework this sits on the eight-tick octave (T7) and the free-group structure of closed walks; it carries no model and no search, only the derived tables needed to trust finished certificates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.