entryOk
plain-language theorem explainer
Boolean check that a pair of 2×2 matrices over Z/3Z are mutual inverses and both have determinant one, i.e. form an inverse pair inside SL(2, Z/3Z). Anyone building or validating a Loom generator table cites it as the per-entry well-formedness gate. It is a pure definition: four decidable equalities conjoined, with no proof obligation.
Claim. Given a pair $(M,N)$ of $2\times 2$ matrices with entries in $\mathbb{Z}/3\mathbb{Z}$, return true if and only if $MN=I$, $NM=I$, $\det M=1$, and $\det N=1$.
background
Loom certifies finished configurations of closed recognition walks on the eight-state, three-axis window fixed by the forcing chain. Closed walks up to homotopy form a free group of rank five; a configuration is a finite list of reduced words sharing a basepoint. The module supplies a total well-formedness checker and a computable invariant valued in traces (and commutator traces) inside $SL(2,\mathbb{Z}/3\mathbb{Z})$.
Matrices are the hand-rolled structure Mat with four ZMod 3 components, chosen so thousands of products reduce inside the kernel without Finset.sum. A table is a list of pairs: for each generator, the image matrix and the image of its inverse. The invariant is a class function, so conjugation-blindness is a ring identity rather than a canonicalisation step.
The local setting is certificate language only: no model, no search. Data that claim to be generator images must be checkable rather than trusted; that is the role of this predicate and of the list-wide wrapper that applies it to every pair.
proof idea
Definition, not a theorem. The body is the Boolean conjunction of four decidable equalities: left and right products equal the identity matrix, and both determinants equal one. No lemmas are invoked; reduction is by the derived DecidableEq instance on Mat and the ring operations already defined on it.
why it matters
This is the atomic well-formedness gate for Loom tables. Table.ok is exactly T.all entryOk, and the module doc states that a table defines a free-group homomorphism precisely when each pair is an inverse pair inside the determinant-one subgroup. Downstream theorems entryOk_matAt, entryOk_one, det_letterMat, and letterMat_mul_neg unpack a successful check into the concrete facts that letter images have det 1 and that positive and negative letters multiply to the identity. Those facts feed ok_tableOfSubst and the evaluation of words and substitutions, which in turn underwrite the conjugation-blind trace invariant on the free group of rank five. Without a decidable per-entry test, the certificate language could not refuse malformed generator data before computing traces.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.