ok_tableOfSubst
plain-language theorem explainer
If a generator table into SL(2, Z/3Z) is well-formed, every table obtained by substituting words for the five free generators remains well-formed. Separation cites this to certify all forty-eight automorphism images of the base table without trusting extra data. The proof evaluates each substituted word, applies the det-one adjugate identities, and checks the three entryOk conditions.
Claim. Let $T$ be a table assigning to each free generator a pair of matrices in $\mathrm{SL}(2,\mathbb{Z}/3\mathbb{Z})$ that are mutual inverses of determinant one, and let $\sigma$ send each generator to a word. Then the table whose entries are the $T$-evaluations of those words (paired with the evaluations of their free inverses) is again well-formed.
background
Loom is a certificate language for finished configurations of closed recognition walks on the eight-state, three-axis window fixed by the forcing chain. Closed walks up to free reduction form a free group of rank five; a configuration is a finite list of such words sharing a basepoint. Content is blind to free reduction and to simultaneous conjugation, so the module supplies a total well-formedness checker and a computable invariant (traces and pairwise commutator traces in $\mathrm{SL}(2,\mathbb{Z}/3\mathbb{Z})$) that ignores exactly those operations.
A table is a list of matrix pairs: for each generator, the image and the image of its inverse. Well-formedness (Table.ok) demands that each pair multiplies both ways to the identity and that both determinants equal one, i.e. a homomorphism into $\mathrm{SL}(2,\mathbb{Z}/3\mathbb{Z})$. A substitution is a list of words, one per generator: the data of a window automorphism acting on the free generators by sending each to a word.
The map tableOfSubst rebuilds a table by evaluating those words (and their free inverses) under the original table. Upstream lemmas supply word evaluation, free inversion of words, determinant of evaluated words under a well-formed table, and the matrix identities mul_adj_of_det_one / adj_mul_of_det_one that recover the identity from a det-one matrix and its adjugate.
proof idea
Unfold well-formedness to a universal quantifier over mapped entries, and unpack tableOfSubst as a list map. For an arbitrary generator word $g$ appearing in the substitution, obtain $\det(\mathrm{eval}_T g)=1$ from det_evalWord and the hypothesis that $T$ is well-formed. Identify $\mathrm{eval}_T(g^{-1})$ with the adjugate of $\mathrm{eval}_T g$ via evalWord_invWord. The two products then reduce to the identity by rewriting through Mat.mul_adj_of_det_one and Mat.adj_mul_of_det_one (with Mat.mul_def / Mat.one_def). Determinant of the inverse image follows from Mat.det_adj. The three boolean conjuncts of entryOk then simplify to true.
why it matters
This is the algebraic engine that lets Separation trust only the single base table. Downstream, base_ok decides that the five generator images really are inverse pairs of determinant one, and tableOfSubst_ok is the one-line application
ok_tableOfSubst base base_ok σ,
so every one of the forty-eight window automorphisms yields a well-formed table computed by Lean rather than supplied as trusted data.
In the Loom story that matters: the invariant must be checked on a full orbit under the 48 automorphisms of the eight-tick, three-axis window (the same quotient that forces $D=3$ and the period-$2^3$ octave in the forcing chain). Without preservation of well-formedness under substitution, each relabelled table would be an independent hypothesis. The module carries no model and no search; this lemma is what keeps the certificate side total and closed under the non-content operations the header isolates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.