base
plain-language theorem explainer
Static certificate table recording the measured homomorphism from the free group of rank five into SL(2, Z/3Z). Loom separation and gauge-invariance checks cite it as the fixed map under which the witness pair is depth-one and abelian-indistinguishable. The body is emitted data from certificate.json, not a derived proof.
Claim. Let $F_5$ be the free group of rank five and $G=\mathrm{SL}(2,\mathbb{Z}/3\mathbb{Z})$. The constant $\mathrm{base}$ is the ordered table of five entries in $G$ (each entry a pair of length-four vectors over $\mathbb{Z}/3\mathbb{Z}$) that records the images of the free generators under the homomorphism found by the Loom search.
background
This module holds the measured Loom certificate as Lean data, regenerated from certificate.json rather than hand-edited. The ambient target is the determinant-one subgroup of $2\times 2$ matrices over $\mathbb{Z}/3\mathbb{Z}$. A Table is the concrete carrier for a homomorphism out of the free group on five generators; Table.ok is a decidable well-formedness predicate checked on every stored table in the separation module, so a transcription error cannot silently become a theorem.
The theoretical setting is gauge-aware separation of a witness pair of utterances. Forty-eight automorphism tables store composites under $\mathrm{Aut}(Q_3)$, so a gauge image is read by swapping tables rather than rewriting words. What Lean trusts is only provenance of those automorphisms (measured externally); self-tests recover twelve oriented faces at walk length four and ninety-six Hamiltonian walks in one gauge class.
Two encoder configurations sit on top of this homomorphism under a codebook chosen so no length statistic separates the pair (both cost 142 acts). Depth-one and abelianised readings coincide; only depth two differs.
proof idea
No proof. The declaration is a literal data definition: a five-element list of pairs of length-four vectors with coordinates in ${0,1,2}$, emitted by the certificate generator. Well-formedness and homomorphism properties are discharged elsewhere by the decidable Table.ok checks in the separation module, not inside this binding.
why it matters
This table is the single measured homomorphism that the rest of the Loom certificate hangs on. Downstream certificate data (autTables, configuration pairs, substitution configs) compose or reindex against it so gauge images are table swaps. Module-level claims that depend on it include: depth-one readings of the flagship pair identical as $[0,0,2,2,2,2,2]$, matching abelianised readings, and separation only at depth two; a second pair under another codebook is conflated even by parent-child-aware readings and is separated by an explicit model, with both pairs certified by one homomorphism.
In the broader Recognition stack this is infrastructure for making kernel-checkable linguistic separation, not a forcing-chain step (T5–T8) or a mass-ladder identity. It closes the gap between externally searched certificate JSON and machine-checked Lean predicates, so separation theorems quote concrete data rather than axioms about the search.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.