cj
plain-language theorem explainer
Conjugation of a 2×2 matrix X by G over ℤ/3ℤ is the product G X adj(G). Loom users cite it whenever a closed walk’s basepoint is moved: the shared conjugator is the image of the prefix word. The body is a three-factor product; det G = 1 is required only at call sites so adj G acts as the inverse.
Claim. For $G,X\in M_2(\mathbb{Z}/3\mathbb{Z})$, define the conjugate $\mathrm{cj}(G,X):=G\,X\,\mathrm{adj}(G)$, where $\mathrm{adj}$ is the classical adjugate.
background
Loom treats finished recognition histories as finite lists of reduced words in five signed generators (the free group of rank $E-V+1=5$ on the eight-state, three-axis window). Spelling is not content, so words are free-reduced; the starting vertex is not content either, so simultaneous conjugation of every loop by one common word is quotiented out.
Matrices here are bare four-tuples $(a,b,c,d)$ over $\mathbb{Z}/3\mathbb{Z}$, not Mathlib Matrix, so thousands of products reduce inside the kernel. The adjugate supplies the inverse whenever $\det G=1$, which is the SL(2,ℤ/3ℤ) setting in which loop traces and commutator traces are read.
The module’s invariant is a class function on those images: blindness to conjugation is a ring identity, not a canonicalisation step. Conjugation is therefore the algebraic stand-in for “moving the shared basepoint.”
proof idea
Pure definition: expand to the three-factor product $GX\mathrm{adj},G$. No lemmas, no tactics, no hypotheses. Downstream theorems (adj_cj, cj_mul, comm_cj) reintroduce $\det G=1$ when they need $\mathrm{adj},G\cdot G=1$.
why it matters
This is the algebraic primitive behind basepoint independence of the Loom certificate. evalWord_conjWord says evaluating a conjugated word is matrix conjugation of the images; invariantOf_cj (the soundness theorem) and invariant_conjWord lift that to whole configurations, proving the invariant is blind to simultaneous basepoint moves. Commutator conjugation (comm_cj) keeps the depth-two lower-central data that plain loop traces fail to separate among the 48 window automorphisms.
In the Recognition chain the setting is the eight-tick octave (T7) and the free group of closed walks on the forced 3-axis window (T8). The definition itself carries no model; it only equips the total checker that a finished object can be trusted without search.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.