invariant_substConfig
plain-language theorem explainer
Relabelling an utterance and reading it under a fixed homomorphism equals reading the original utterance under the composed homomorphism. Certificate authors cite this so the forty-eight window automorphisms are checked by swapping tables, never by rewriting words. The proof is a short map-congruence through word evaluation under substitution, then a one-step rewrite of the invariant.
Claim. For any homomorphism table $T$ (pairs of matrices for each generator and its inverse), any generator substitution $\sigma$ (a window automorphism sending each of the five free generators to a word), and any configuration $c$ (a finite list of closed walks sharing one basepoint), the invariant of the $\sigma$-substituted configuration under $T$ equals the invariant of $c$ under the table obtained by composing $T$ with $\sigma$.
background
Loom is a certificate language for finished configurations of closed recognition walks on the eight-state, three-axis window forced by the chain. Closed walks up to homotopy form a free group of rank five, so an utterance is a finite list of words in five signed generators at one basepoint. Content is defined by two refusals: free reduction is not content, and simultaneous conjugation of every loop is not content either.
A Table assigns to each generator a pair of matrices in $\mathrm{SL}(2,\mathbb{Z}/3\mathbb{Z})$ (image and inverse image). A Subst is the data of a window automorphism acting on the five generators by words. The computable invariant evaluates each loop (and pairwise commutators of loop images) under the table and reads traces; trace is a class function, so conjugation-blindness is a ring identity rather than a canonicalisation step.
This lemma is the relabelling half of soundness: substituting generators in the utterance is interchangeable with pushing the same substitution into the homomorphism table.
proof idea
First prove the intermediate equality that evaluating the substituted configuration under $T$ equals evaluating the original configuration under the substituted table. Unfold evaluation and substitution; both are list maps, so List.map_map reduces the claim to pointwise agreement on words. For each word, evalWord_substWord supplies the word-level identity. With evaluation equal, unfold the invariant definition and rewrite by that equality. The whole argument is a short tactic script: one intermediate have, map congruence, then a final simp on the invariant.
why it matters
This is the soundness half for window automorphisms: the forty-eight automorphisms of the recognition window are checked by forty-eight tables, and no certificate word is rewritten. Downstream, invariant_gaugeImage chains it with reduction and conjugation invariance to show the full gauge action (substitution, optional flip, conjugation) preserves the invariant after table adjustment. The separation layer's locks codebook choice is free precisely because of this identity: which table is used is a convention, not content.
In the framework this sits on the eight-tick, three-axis window (T7 period $2^3$, T8 spatial $D=3$) whose closed walks supply the free generators. The invariant itself mixes ordinary loop traces with depth-two commutator traces so that abelianised readings cannot separate the intended witness. Certificate data such as the base table is only meaningful up to this table-side transport.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.