evalWord_singleton
plain-language theorem explainer
Evaluating a one-letter word under a generator table returns exactly that letter's matrix. Anyone working the Loom word-to-matrix map cites this as the base case of the homomorphism. The proof is a one-line simplification of the recursive definition against the right-unit law for matrix multiplication.
Claim. For any generator table $T$ and any integer letter $x$, the matrix image of the singleton word $[x]$ equals the matrix that $T$ assigns to $x$.
background
Loom is a certificate language for 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 finished utterance is a finite list of words in five signed generators sharing one basepoint. Content is read up to free reduction and simultaneous conjugation; the module supplies a total well-formedness checker and a computable invariant in $\mathrm{SL}(2,\mathbb{Z}/3\mathbb{Z})$ that is blind to both non-content operations.
A Table pairs, for each generator, the matrix image of the generator with the matrix image of its inverse. letterMat T x looks up the positive or negative entry according to the sign of $x$ (and returns the identity when $x=0$). evalWord is the structural product: empty word maps to $1$, and a cons multiplies the head letter's matrix on the left by the image of the tail. This lemma is the one-letter instance of that product.
proof idea
One-line wrapper. Unfold evalWord on the singleton cons to obtain letterMat T x * evalWord T [], which is letterMat T x * 1 by the empty-word clause. Discharge the trailing unit with mul_one. No case split on the sign of $x$ is needed; that lives inside letterMat.
why it matters
Base case for the word homomorphism into matrix monoids. Downstream, evalWord_consRed uses it when free reduction hits the empty tail, so reduced cons still multiplies as an ordinary letter times the image of the remainder. evalWord_invWord uses it in the inductive step that shows inversion of a word maps to the adjugate (inverse in $\mathrm{SL}(2,\mathbb{Z}/3\mathbb{Z})$) of the word's image. Together those facts let the Loom invariant, built from traces of loop images and their pairwise commutators, ignore free reduction and respect word inversion without canonicalising spelling. That is exactly the "spelling is not content" half of the module's design, on the free group of rank five coming from the eight-tick window ($E-V+1=5$).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.