evalWord_append
plain-language theorem explainer
Concatenating two words and evaluating under a generator table equals the product of the two evaluations. Anyone proving that Loom evaluation is a monoid homomorphism (inverses, conjugations, substitutions) cites this. The proof is induction on the left word, using the empty-word unit law and matrix multiplication associativity.
Claim. For any generator table $T$ and words $u,v$ in the five signed cotree generators, $\mathrm{eval}_T(u{+}{+}v)=\mathrm{eval}_T(u)\,\mathrm{eval}_T(v)$ in the matrix monoid.
background
The Loom module 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 walk is a word in five signed generators (Word := List Int). An utterance is a finite list of such words sharing one basepoint.
A Table assigns to each generator a pair of matrices (image and inverse image). Evaluation evalWord T w multiplies those matrices along the letters of $w$, reading the empty word as the identity. The module's invariant lives in $\mathrm{SL}(2,\mathbb{Z}/3\mathbb{Z})$ and is built from loop traces and pairwise commutator traces, so it needs evaluation to respect list concatenation as monoid multiplication.
Upstream, the proof only needs the monoid laws one_mul and mul_assoc on the matrix side (imported through the foundation arithmetic stack).
proof idea
Term-mode induction on the left word $u$.
- Base: $u=[]$. Then $[]{+}{+}v=v$ and
evalWord T []is the identity, so the claim isone_mul. - Step: $u=x{::}t$. Concatenation and the recursive clause of
evalWordgive a product of three matrices; the inductive hypothesis rewrites the tail, andmul_assocreassociates to match the right-hand side.
No table well-formedness hypothesis is required; the identity is pure list/monoid algebra.
why it matters
This is the basic monoid-homomorphism law for Loom evaluation. Downstream it is the workhorse for three structural theorems: evalWord_invWord (inverses map to adjugates), evalWord_conjWord ("Moving one loop's basepoint is conjugating its image"), and evalWord_substWord (relabelling words equals changing the table, so the forty-eight window automorphisms can be checked by table change rather than word rewrite).
Those facts underwrite the module's claim that the computable invariant is blind to free reduction and simultaneous conjugation, the two non-content operations on finished recognition histories. In the broader RS picture this sits on the eight-tick, $D=3$ window (T7–T8) whose closed walks supply the free generators being evaluated.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.