evalWord_invWord
plain-language theorem explainer
Evaluating the free-group inverse of a closed-walk word under a well-formed generator table yields the adjugate of the original matrix image in SL(2,Z/3Z). Anyone proving conjugation invariance or that the Loom configuration invariant is blind to simultaneous loop reversal cites this identity. The proof is induction on the word, using the two-by-two adjugate antimorphism and the table's signed-letter law.
Claim. Let $T$ be a well-formed table of generator matrices in $\mathrm{Mat}_{2}(\mathbb{Z}/3\mathbb{Z})$ (each generator paired with its inverse image). For every word $w$ in the five signed cotree generators, the evaluation of the free-group inverse word equals the adjugate of the evaluation of $w$: $\mathrm{eval}(T,w^{-1})=\mathrm{adj}(\mathrm{eval}(T,w))$.
background
Loom treats finished recognition histories as finite lists of closed walks on the eight-state, three-axis window. Up to homotopy those walks are words in a free group of rank five; an utterance is a list of such words sharing one basepoint. Content is quotiented by free reduction and by simultaneous conjugation, so the module supplies a total well-formedness checker and a computable invariant blind to exactly those operations.
Matrices are stored by components over $\mathbb{Z}/3\mathbb{Z}$ rather than as abstract Matrix values, because later kernel evaluation multiplies thousands of them. The adjugate $\mathrm{adj}(X)=\langle d,-b,-c,a\rangle$ is total and coincides with the inverse on every matrix the module produces (determinant one). A table assigns to each generator both its image and the image of its inverse; well-formedness (Table.ok) enforces that pairing.
Upstream, adj_mul records the ring identity $\mathrm{adj}(XY)=\mathrm{adj}(Y),\mathrm{adj}(X)$ with no determinant hypothesis, and adj_one fixes the unit. Those two facts, together with the signed-letter evaluation law, drive the induction below.
proof idea
Induct on the word $w$.
Nil case: the inverse of the empty word is empty, evaluation is the identity matrix, and adj_one gives $\mathrm{adj}(1)=1$.
Cons case $w=x::t$: rewrite the inverse as the reverse-append of the tail inverse with the negated letter (invWord_cons). Evaluation splits by evalWord_append. The inductive hypothesis replaces the tail inverse by an adjugate. The negated letter evaluates to the adjugate of the letter matrix (letterMat_neg, using well-formedness of $T$). Reassociating with evalWord_cons and applying adj_mul yields $\mathrm{adj}(\mathrm{letter}\cdot\mathrm{eval}(t))$, as required.
why it matters
The Loom invariant reads traces of loop images and of their pairwise commutators in $\mathrm{SL}(2,\mathbb{Z}/3\mathbb{Z})$. Trace is a class function, so conjugation blindness is a ring identity; this lemma supplies the inverse half of that identity. Downstream, evalWord_conjWord builds conjugation of a loop image from append plus this inverse law, and invariant_map_invWord concludes that reversing every loop of an utterance leaves the invariant unchanged. The same equality appears inside ok_tableOfSubst, confirming that substituted tables remain well-formed because the inverse slot really is the adjugate of the evaluation.
In the broader Recognition picture the free group of rank five is the closed-walk group on the eight-tick window forced by T7–T8. The lemma is pure linear algebra over that window; it does not itself force dimension or the octave, but it is load-bearing for the certificate language that checks finished configurations without rebuilding them.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.