evalWord_reduceWord
plain-language theorem explainer
Free reduction leaves the matrix image of a closed walk unchanged: under any well-formed generator table, evaluating a word equals evaluating its freely reduced form. Cited by anyone proving the Loom invariant is blind to spelling, and by the conjugation identity for basepoint moves. Proof is induction on the word list, rewriting through the cons-reduction and evaluation lemmas.
Claim. Let $T$ be a well-formed table assigning to each of the five signed generators a pair of matrices in $\mathrm{SL}(2,\mathbb{Z}/3\mathbb{Z})$ (image and inverse image). For every word $w$ in those generators, the matrix product obtained by evaluating the freely reduced form of $w$ equals the matrix product obtained by evaluating $w$ itself.
background
Loom treats finished recognition histories as finite lists of closed walks on the eight-state, three-axis window forced by the chain (period $2^3$, $D=3$). Up to homotopy those walks form a free group of rank $E-V+1=5$, so each loop is a word in five signed generators (Word is a list of integers). An utterance is a finite list of such words sharing one basepoint.
Content is defined by two refusals. Spelling is not content: words are identified up to free reduction (cancel adjacent inverse pairs). Starting vertex is not content either: simultaneous conjugation of every loop is gauge. The module supplies a total well-formedness checker, a computable invariant valued in traces in $\mathrm{SL}(2,\mathbb{Z}/3\mathbb{Z})$, and theorems that the invariant is blind exactly to those two operations.
A Table assigns to each generator the matrix it maps to and the matrix its inverse maps to. Evaluation multiplies those matrices along the word. The hypothesis Table.ok T = true guarantees the table respects inverses and lands in the monoid where the reduction lemmas apply.
proof idea
Term-mode induction on the word list $w$.
- Empty word: both sides evaluate to the identity;
rfl. - Cons case $x::t$: rewrite with
reduceWord_cons(how free reduction acts on a head generator), thenevalWord_consRed(evaluation of the reduced cons equals evaluation of the unreduced cons when the table is well-formed), apply the inductive hypothesis on the tail, and finish withevalWord_cons(evaluation of an unreduced cons is head matrix times tail evaluation).
No separate case split on whether the head cancels: that bookkeeping lives inside reduceWord_cons and evalWord_consRed.
why it matters
This is the algebraic half of "spelling is not content" in the Loom certificate language. Downstream, invariant_reduceConfig lifts the equality from single words to whole configurations, so the trace-and-commutator invariant is unchanged by normalising every loop. The sibling evalWord_conjWord also rewrites through this theorem when it expands conjugation as inverse-append-reduce, turning basepoint moves into matrix conjugation.
In the framework, closed walks live on the eight-tick octave forced at $D=3$ (T7/T8). The free group of rank five is the homotopy type of that window; free reduction is the free-group relation that must be invisible to any observable. Without this equality the invariant could not be trusted as a certificate of a finished object the checker did not build. It closes no open scaffold: it is a proved lemma inside an already total checker.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.