Table
plain-language theorem explainer
A table is a finite list of matrix pairs over Z/3Z, one pair per free generator: the image of the generator and the image of its inverse. Anyone building or checking Loom certificates cites this as the raw data type of a homomorphism from the free group of closed walks. It is a one-line type synonym for List of Mat pairs; well-formedness is checked separately.
Claim. A table is a list of pairs $(M, M^{-1})$ of $2\times 2$ matrices with entries in $\mathbb{Z}/3\mathbb{Z}$, one pair for each free generator of the closed-walk group: the first component is the image of the generator and the second is the image of its inverse.
background
The Loom module is a certificate language for 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 $E-V+1=5$, so a finished utterance is a finite list of words in five signed generators sharing one basepoint. Content is read up to free reduction and simultaneous conjugation; the module supplies a total well-formedness checker and a computable invariant blind to those two operations.
Matrices are not Mathlib Matrix values. Mat is a four-component structure $(a,b,c,d)$ over $\mathbb{Z}/3\mathbb{Z}$, chosen so that thousands of products reduce cheaply in the kernel. The invariant lives in $\mathrm{SL}(2,\mathbb{Z}/3\mathbb{Z})$: traces of loop images and of their pairwise commutators (depth-two lower-central data).
A table packages, for each generator, the pair of matrices that a homomorphism must send the generator and its inverse to. The companion predicate entryOk demands that the pair multiplies to the identity both ways and that both determinants equal one, so the list really defines a homomorphism into the determinant-one subgroup.
proof idea
One-line type synonym: Table is defined as List (Mat × Mat). There is no proof obligation. Well-formedness, determinant preservation under word evaluation, and the conjugation-blind invariant are proved later against this carrier type.
why it matters
Every concrete Loom certificate is a value of this type. Downstream, base is the search-found homomorphism and autTables is the list of forty-eight composite tables, one per automorphism of the window $Q_3$. Evaluation lemmas (evalWord, det_letterMat, det_evalWord, entryOk_matAt, evalConfig) all take a table as the homomorphism data and prove that reduced words land in $\mathrm{SL}(2,\mathbb{Z}/3\mathbb{Z})$.
In the Recognition framework this is the data layer under the eight-tick octave and the free-group description of closed walks (rank five on the forced window). Trace is a class function, so conjugation blindness is a ring identity rather than a canonicalisation step; tables feed that invariant without carrying a model or a search. The type itself settles no open question; it is the shared carrier that lets certificate data, automorphism orbits, and the total checker speak the same language.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.