base_ok
plain-language theorem explainer
The base generator table for the Loom separation witness is a valid homomorphism from the free group of rank five into SL(2, Z/3Z): each of the five images is an inverse pair of determinant one. Anyone citing the gauge-invariant separation of the two weave witnesses needs this fact as trusted input. The proof is a pure kernel decide check on a finite boolean predicate; nothing is assumed.
Claim. The base table of five generator images consists of inverse pairs of determinant one in $\mathrm{SL}(2,\mathbb{Z}/3\mathbb{Z})$, so it defines a group homomorphism from the free group of rank five into $\mathrm{SL}(2,\mathbb{Z}/3\mathbb{Z})$. The predicate evaluating this table returns true.
background
The Loom separation module compares two weave utterances that agree under every depth-one and abelianised reading, yet differ under the commutator (depth-two) reading. The semantic carrier is a homomorphism from the free group on five generators into the finite group $\mathrm{SL}(2,\mathbb{Z}/3\mathbb{Z})$. A table records the five generator images; the predicate Table.ok asserts that each image is an inverse pair of determinant one, i.e. that the assignment extends to a genuine homomorphism.
Only the base table is trusted data. The forty-eight automorphisms of the recognition window act by substitution on generators; each composite table is computed in Lean from that action rather than supplied by hand. The module then shows that no gauge image of witness A equals witness B, so the pair are distinct meanings rather than two spellings of one.
Local setting (from the module header): counting one-bit acts and loop-length multisets cannot separate the pair; the separation is carried by the depth-two invariant and by exhaustive gauge coverage of order 96 times free basepoint choice.
proof idea
One-line kernel decision. The goal is the boolean equality Table.ok base = true. Because the table is a concrete finite object in $\mathrm{SL}(2,\mathbb{Z}/3\mathbb{Z})^5$ and the ok-predicate is decidable (inverse-pair and determinant-one checks on $2\times 2$ matrices over a three-element ring), decide closes the goal with no lemmas and no hypotheses.
why it matters
This is the single trusted seed for the whole separation stack. Downstream, tableOfSubst_ok lifts the fact to every automorphism image via ok_tableOfSubst, so no table beyond the base is trusted data. invariant_gaugeImage rewrites the depth-two invariant under gauge action using base_ok to justify reduction and conjugation lemmas. The end theorem witnesses2_separated then concludes that no gauge image of one weave equals the other.
In framework terms the result sits inside the Loom domain: it certifies that the semantic carrier used for the separation witness is a real homomorphism into the finite recognition window group, not an ad-hoc assignment. The module header stresses that the gauge group quotiented over has order 96 times free basepoint choice and that the two invariants differ in one coordinate of twenty-one (the smallest exact margin). Without a decided base table, none of that gauge coverage is honest.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.