matAt_tableOfSubst
plain-language theorem explainer
Looking up the nth generator image in a table built by applying a generator-to-word substitution yields the pair of matrix evaluations of that word and its free inverse. Anyone composing window automorphisms with the SL(2,Z/3) Loom invariant cites this bridge. The proof is a short induction on the substitution list with case splits on the index.
Claim. For any matrix table $T$, substitution $\sigma$ (a list of words on the five generators), and index $n\in\mathbb{N}$, the $n$th entry of the table obtained by substituting $\sigma$ into $T$ equals $\bigl(\mathrm{eval}_T(w_n),\,\mathrm{eval}_T(w_n^{-1})\bigr)$, where $w_n$ is the $n$th word of $\sigma$ (empty when out of range).
background
Loom is a certificate language for finished configurations of closed recognition walks on the eight-state, three-axis window fixed by the forcing chain. Closed walks up to homotopy form a free group of rank five, so a configuration is a finite list of words in five signed generators. The module supplies a total well-formedness checker and a computable invariant valued in traces in $\mathrm{SL}(2,\mathbb{Z}/3)$, including pairwise commutator traces at depth two of the lower central series.
A table assigns to each generator a matrix and the matrix of its inverse. A substitution is the data of a window automorphism acting on generators: a list of words, one image per generator. Word evaluation is the structural product of letter matrices under a fixed table (empty word maps to the identity). The substituted table rebuilds those pairs by evaluating each substitution word and its free inverse under the original table; this lemma identifies the pointwise lookup with that construction.
proof idea
Term-mode induction on the substitution list $\sigma$, generalizing the index $n$.
Empty substitution: both $n=0$ and $n=\mathrm{succ},m$ reduce by reflexivity (out-of-range lookup and empty-word evaluation agree with the definitions of table construction and word evaluation).
Cons case $g::t$: at $n=0$ the head of the substituted table is definitionally $(\mathrm{eval}_T(g),\mathrm{eval}_T(g^{-1}))$, so reflexivity; at $n=\mathrm{succ},m$ the claim is exactly the inductive hypothesis on the tail at index $m$. No external lemmas are required beyond the recursive definitions of table-of-substitution, word lookup, and evaluation.
why it matters
This is the table-level bridge used immediately by the letter-substitution identity: evaluating a substituted signed letter under $T$ equals reading the letter matrix from the substituted table. That step is how window automorphisms (relabellings of the five generators by words) are pushed through the matrix representation before traces are taken.
In the Loom architecture the invariant must be blind to the two non-content operations: free reduction of spelling, and simultaneous conjugation (basepoint change). Automorphisms of the recognition window are the third quotient the module must respect; the module doc ties them to the same label-independence that motivates quotienting by the 48 window automorphisms. Without this lookup identity, substituted configurations could not be scored by reusing the original table evaluator. It sits entirely inside the certificate layer: no model, no search, only the algebraic interface the checker trusts.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.