gaugeImage
plain-language theorem explainer
The gauge image of an utterance is the free reduction after generator relabeling by a window automorphism, optional simultaneous loop reversal, and basepoint conjugation by a fixed word. Separation theorems cite it to prove no gauge transform of witness A equals B (and likewise for C versus D). The body is a three-step composition: substitute, optionally invert every loop, conjugate, then reduce.
Claim. For a generator substitution $\sigma$, a boolean flag $f$, a conjugating word $g$, and an utterance $c$ (a finite list of closed walks sharing one basepoint), the gauge image is the free reduction of the list obtained by applying $\sigma$ to every loop of $c$, optionally replacing each loop by its reverse-with-negated-acts when $f$ is true, then conjugating every resulting loop by $g$.
background
In the Loom, an utterance (configuration) is a finite list of closed walks on the recognition window that share one basepoint. Free reduction respells each walk by cancelling adjacent inverse acts. Conjugation by a word $g$ moves that shared basepoint: each loop $w$ becomes the reduced word $g,w,g^{-1}$. Inversion of a single loop reverses the walk and negates every act; applied to every loop at once it is treated as gauge rather than content.
The Separation module compares two pairs of utterances that encode dual quantifier patterns over the same ground facts ("every door has a key that opens it, and one master key locks all" versus the security-hole dual). Depth-one and abelianised readings are identical on each pair; the commutator reading differs. To conclude the pairs are distinct meanings rather than spellings, one must quotient by the full gauge action: automorphisms of the window, simultaneous reversal, basepoint moves, free respelling, and loop reordering (the last handled by a permutation hypothesis, since an utterance is a multiset).
This definition packages the continuous part of that action. The discrete automorphism membership and the permutation hypothesis sit on the theorems that consume it.
proof idea
Pure definition, not a proof. Substitute generators via $\sigma$ on every loop of $c$. If the flip flag is true, map every loop through word inversion (reverse and negate acts); otherwise leave the substituted list alone. Map every loop through conjugation by $g$ (basepoint move). Finish with free reduction of the whole configuration. No lemmas are invoked inside the body; downstream theorems rewrite through this composition using the separate invariance lemmas for reduction, conjugation, substitution, and inversion.
why it matters
This is the operational form of gauge used by the separation theorems. no_gauge_image_of_A_is_B (and its C/D twin) state that for every automorphism substitution, every flip choice, every basepoint word, and every free respelling-plus-reordering, the image of A is not B: the two are different meanings while every depth-one reading conflates them. The module doc records the strength: the gauge group quotiented has order 96 times free basepoint choice, all 48 automorphisms are covered exactly, and the invariants differ in one coordinate of twenty-one.
invariant_gaugeImage shows the depth-two invariant is unchanged (up to the induced base table) under this action, so inequality of invariants after any gauge image is a genuine content distinction. Downstream wrappers gauge_image_ne_B, gauge_image_ne_D, witnesses_separated, and witnesses2_separated restate the same fact at the level of the woven utterances themselves. Without a single named gauge-image map, those statements would scatter the same four operations across every hypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.