substConfig
plain-language theorem explainer
Pointwise application of a generator relabelling to every loop in an utterance. Configurations are finite lists of closed walks on the five-generator free group of the eight-tick window; a substitution sends each generator to a word. Anyone proving gauge invariance of the Loom trace invariant cites this map. The body is a one-line List.map of the word-level substitution.
Claim. Given a relabelling $\sigma$ of the five generators (each sent to a word) and an utterance $c$ (a finite list of closed walks sharing a basepoint), the substituted configuration is the list obtained by applying the induced word map of $\sigma$ to every loop in $c$.
background
Loom treats finished recognition histories as closed walks on the eight-state, three-axis window forced by the T0–T8 chain. Up to free homotopy those walks form a free group of rank $E-V+1=5$, so an utterance is a finite list of words in five signed generators sharing one basepoint.
A substitution (relabelling) is the data of an automorphism of the recognition window acting on generators: each generator is sent to a word. Configurations are just lists of such words. Spelling is not content, so words are later read up to free reduction; basepoint choice is not content either, handled by simultaneous conjugation.
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 to the two non-content operations. Trace is a class function, so conjugation-blindness is a ring identity rather than a canonicalisation step.
proof idea
One-line definitional wrapper: the configuration is a List Word, and the substituted configuration is that list mapped by the already-defined word-level substitution induced by $\sigma$. No lemmas are invoked; Lean constructs the composite tables from the relabelling data, so they are not trusted external input.
why it matters
This is the configuration-level action of window automorphisms. Downstream, invariant_substConfig proves the soundness half for relabelling: reading a relabelled utterance equals reading the original under the relabelled homomorphism, so the forty-eight automorphisms of the window are checked by forty-eight tables without rewriting words. Downstream gaugeImage builds a full gauge orbit by composing this substitution with optional global inversion, basepoint conjugation, and free reduction.
In the Recognition framework the forty-eight automorphisms are the discrete symmetry of the eight-tick octave (T7) with $D=3$ spatial axes (T8). Quotienting by them is the same refusal to let observables depend on labels the description supplies. The definition therefore sits on the path that makes the Loom invariant a genuine certificate of content rather than of spelling or basepoint.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.