entryOk_matAt

Loom is a certificate language for finished configurations of closed recognition walks on the eight-state, three-axis window. Closed walks up to free reduction and simultaneous conjugation are words in five signed generators; a configuration is a finite list of such words. The module supplies a total well-formedness checker and a computable invariant valued in traces and commutator traces in $\mathrm{SL}(2,\mathbb{Z}/3\mathbb{Z})$.

A table is a list of matrix pairs, one pair per generator: the image of the generator and the image of its inverse. An entry is well-formed when the two matrices multiply both ways to the identity and both have determinant one. That Boolean predicate is exactly the local condition for the table to define a homomorphism from the free group into the determinant-one matrices. Indexing a table at a natural number returns the corresponding pair, or the identity pair when the index runs past the end.

The empty-table base case is settled by the identity pair being well-formed (proved by decision).

Term-mode induction on the table $T$, generalizing the index $n$.

• Empty table: matAt returns the identity pair, and entryOk_one says that pair is well-formed.
• Cons cell $e::t$: unpack Table.ok as the conjunction that $e$ is well-formed and the tail is well-formed. Case-split on $n$. At zero, matAt returns $e$, so the head conjunct finishes it. At successor $m$, apply the inductive hypothesis to the tail with the tail conjunct as the well-formedness hypothesis.

No ring identities are needed; the argument is pure list structure and Boolean unpacking.

Letter matrices are built by looking up table entries at generator indices. Two immediate parents need those lookups to be well-formed: det_letterMat (every letter matrix has determinant one) and letterMat_mul_neg (a letter and its formal inverse multiply to the identity). Both open by invoking this theorem on x.natAbs - 1 and unpacking the four Boolean conjuncts.

Together those facts place the free-group homomorphism inside $\mathrm{SL}(2,\mathbb{Z}/3\mathbb{Z})$, which is the ring in which the Loom invariant reads traces and pairwise commutator traces. Without entry-level well-formedness, the invariant would not be defined on a genuine group image, and blindness to free reduction and conjugation would not be ring identities. The result sits entirely inside the Loom certificate layer; it does not touch the forcing chain (T0–T8) or the mass ladder, but it is load-bearing for every configuration certificate that uses the table homomorphism.