evalWord_substLetter
plain-language theorem explainer
Single-letter substitution commutes with matrix evaluation: the image of a signed generator under a window relabelling, read in table T, equals that generator read in the pushed-forward table. The word-level homomorphism theorem cites it as the inductive step. Proof is definitional rewrite plus a three-way case split on the sign of the letter index.
Claim. Let $T$ be a homomorphism table (pairs of matrices for each generator and its inverse) and $\sigma$ a substitution (each of the five generators sent to a word). For every integer letter index $x$, evaluating the substituted letter $\sigma(x)$ under $T$ equals the letter-matrix of $x$ under the composed table $T\circ\sigma$.
background
Loom is a certificate language for closed recognition walks on the eight-state, three-axis window. Closed walks up to free homotopy form a free group of rank five, so a finished utterance is a finite list of words in five signed generators sharing one basepoint. Content is blind to free reduction and to simultaneous conjugation; the computable invariant reads traces (and pairwise commutator traces) in $\mathrm{SL}(2,\mathbb{Z}/3\mathbb{Z})$.
A Table assigns to each generator the matrix it maps to and the matrix its inverse maps to. A Subst is the data of a window automorphism acting on generators: each generator is sent to a word. Letter evaluation picks the forward or inverse matrix according to the sign of the integer index (and the identity at zero). The composed table tableOfSubst T σ is the homomorphism obtained by reading those substituted generator-words under $T$.
This lemma is the single-generator fragment of the statement that reading a relabelled utterance under $T$ is the same as reading the original utterance under the relabelled table.
proof idea
Term-mode proof by rewriting and case analysis. Unfold substLetter, letterMat, and the pointwise identity matAt_tableOfSubst that says the composed table at index $x$ is exactly the evaluation of the substituted letter. Split on $0 < x$: both sides take the positive branch and match. On the complementary side, split on $x < 0$: both sides take the negative (inverse) branch and match. The remaining case is $x = 0$, where both sides reduce to the same identity matrix by rfl.
why it matters
Parent theorem is evalWord_substWord, which lifts the letter identity to full words by induction (cons step applies this lemma, then evalWord_append and evalWord_cons). That word-level result is what lets the forty-eight automorphisms of the recognition window be checked by changing the table rather than rewriting every word, and the module header stresses it is a theorem rather than an assumption.
In the Loom story this closes the gap between spelling-level relabelling and the invariant: the checker can push automorphisms into the homomorphism table and keep the utterance fixed. It sits under the free-group rank-five structure forced by the eight-tick window (T7) and the $D=3$ spatial forcing (T8), and supports the claim that the trace-plus-commutator invariant is blind exactly to the two non-content operations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.