adj_one

Loom treats closed recognition walks on the eight-state, three-axis window as words in a free group of rank five. Configurations are finite lists of such words; content is read up to free reduction and simultaneous conjugation. The computable invariant evaluates words in $\mathrm{SL}(2,\mathbb{Z}/3\mathbb{Z})$ and records traces of the images and of their pairwise commutators.

Matrices are stored as a four-component structure Mat over $\mathbb{Z}/3\mathbb{Z}$ rather than a generic matrix type, so that thousands of products reduce inside the kernel. The adjugate is the total map sending $\langle a,b,c,d\rangle$ to $\langle d,-b,-c,a\rangle$; on determinant-one matrices it is the group inverse. The multiplicative identity is the matrix with diagonal ones and off-diagonal zeros.

One-line wrapper: by decide. Both sides are concrete four-tuples in a finite decidable type, so the kernel compares components after unfolding the definitions of the identity and of the adjugate. No lemmas are invoked.

Feeds the nil case of evalWord_invWord, which states that evaluating the free-group inverse of a word yields the adjugate of the evaluation of the word. That identity is required so the Loom invariant is blind to free reduction: inverted syllables must map to matrix inverses, and the empty word is the identity matrix. In the broader Recognition setting this sits inside the certificate layer for closed walks on the eight-tick window (T7), not inside the forcing chain itself; it is pure linear algebra over $\mathbb{Z}/3\mathbb{Z}$ supporting the trace-and-commutator invariant.