entryOk_one
plain-language theorem explainer
The identity pair in SL(2, Z/3Z) passes the Loom entry well-formedness check: mutual inverses and unit determinant. Cited as the nil base case when proving every table entry of a well-formed table is valid. Proof is a one-line kernel decision on the four Boolean conjuncts.
Claim. Let $I$ be the $2\times 2$ identity matrix over $\mathbb{Z}/3\mathbb{Z}$. Then the pair $(I,I)$ satisfies the entry predicate: $I\cdot I = I$, both factors have determinant $1$, so the pair is an inverse pair inside $\mathrm{SL}(2,\mathbb{Z}/3\mathbb{Z})$.
background
Loom is a certificate language for configurations of closed recognition walks on the eight-state, three-axis window. Closed walks up to homotopy form a free group of rank five; a finished utterance is a finite list of reduced words sharing a basepoint. The module supplies a total well-formedness checker, a computable invariant in $\mathrm{SL}(2,\mathbb{Z}/3\mathbb{Z})$, and theorems that the invariant is blind to free reduction and simultaneous conjugation.
Matrices are stored as four components $a,b,c,d\in\mathbb{Z}/3\mathbb{Z}$ rather than Mathlib matrices, so thousands of products reduce cheaply in the kernel. An entry is a pair of such matrices. The predicate entryOk holds exactly when the two factors multiply both ways to the identity and each has determinant one: that is the data of an inverse pair inside the determinant-one subgroup, which is what makes a table define a homomorphism from the free group.
proof idea
One-line computational proof: by decide. All four conjuncts (both products equal the identity matrix, both determinants equal one) are decidable equalities on ZMod 3 components and evaluate to true for the identity pair.
why it matters
Base case for entryOk_matAt, which states that every indexed entry of a well-formed table satisfies the entry predicate. That lemma is the inductive step connecting table-level well-formedness (Table.ok) to per-entry homomorphism data. Without the identity pair being valid, the empty-table (nil) case of the induction would fail, and the total checker could not certify the empty configuration. In the broader Loom story this sits under the certificate layer that trusts finished objects it did not build: no model, no search, only decidable well-formedness and a conjugation-blind trace invariant (including depth-two commutator traces). It does not itself touch the forcing chain (T5–T8) or the mass ladder; it is infrastructure for reading closed walks as free-group words in the eight-tick window.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.