invariant_reduceConfig
plain-language theorem explainer
Free reduction of every loop in a closed-walk configuration leaves the SL(2, Z/3Z) trace invariant unchanged. Anyone proving that Loom certificates ignore spelling (weave reduction, gauge images, conjugation) cites this equality. The proof reduces to word-level evaluation invariance under free reduction, then lifts by list map congruence.
Claim. Let $T$ be a well-formed generator table (each generator paired with a matrix and its inverse in $\mathrm{SL}(2,\mathbb{Z}/3\mathbb{Z})$) and let $c$ be a configuration (finite list of words at a common basepoint). If $c'$ is obtained by freely reducing every word of $c$, then the Loom invariant of $c'$ equals the invariant of $c$: $\mathrm{inv}_T(c')=\mathrm{inv}_T(c)$.
background
Loom treats a finished recognition history as a finite list of closed walks on the eight-state, three-axis window forced by the T0–T8 chain (rank $E-V+1=5$ free group). A configuration is that list of words; a table assigns to each signed generator a matrix in $\mathrm{SL}(2,\mathbb{Z}/3\mathbb{Z})$ and the matrix of its inverse.
Two operations are declared non-content: free reduction (spelling) and simultaneous conjugation of every loop (basepoint). The module’s computable invariant reads traces of the loop images and of their pairwise commutators, so it is a class function and automatically conjugation-blind at the ring level.
The local claim is the spelling half: reducing each word must not change the invariant. Upstream, word evaluation already respects free reduction once the table is well-formed (evalWord_reduceWord); configuration evaluation is the list map of word evaluation.
proof idea
First prove that configuration evaluation is unchanged by reduction: unfold evalConfig and reduceConfig, rewrite the double map, and apply list map congruence. On each word the hypothesis Table.ok T plus evalWord_reduceWord gives equality of matrix images. Then unfold the invariant and substitute that evaluation equality; the invariant is built only from those images (traces and commutator traces), so it matches.
why it matters
This is one of the two blindness theorems the Loom header promises: spelling is not content. Downstream, invariant_weave_reduce is a one-line application showing woven grammar expressions are invariant under how loops are spelled; invariant_gaugeImage rewrites through this fact before conjugation and substitution; abelBag sits beside it as the depth-one (abelianised) reading that deliberately throws commutators away.
In the Recognition frame the result is bookkeeping for certificates of closed walks on the eight-tick window (T7), not a new forcing step. It lets finished objects be checked without caring how generators cancel in the free group, which is required before separation or gauge arguments can treat two spellings as the same witness.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.