tableOfSubst_ok
plain-language theorem explainer
Every automorphism image of the base Loom homomorphism table remains a valid table (determinant-one evaluations on generators). Anyone checking the 48-window gauge orbit of the separation witness cites this. The proof is a one-line application of the general substitution-stability lemma to the certified base table.
Claim. For every substitution $\sigma$ of the recognition-window generators, the table obtained by transporting the base homomorphism along $\sigma$ still satisfies the table-ok predicate (every generator word evaluates to a matrix of determinant $1$).
background
The Loom separation module compares two utterances A and B that share the same multiset of ground facts and the same one-bit act costs, yet differ under a depth-two commutator reading. The gauge group of the recognition window has 48 automorphisms; the module must show no gauge image of A equals B.
A Table is a finite list of generator-to-matrix assignments encoding a homomorphism into $2\times 2$ matrices over a small ring. The predicate Table.ok asserts that every word evaluates with determinant $1$ (and the inverse-word identity holds). The constant base is the concrete homomorphism found by exhaustive search:
$[(⟨2,2,1,0⟩,⟨0,1,2,2⟩),\ldots]$ five pairs.
Upstream, ok_tableOfSubst already proves: if $T$ is ok and $\sigma$ is any substitution, then the transported table tableOfSubst T σ is ok. The present lemma specialises that fact to the trusted base table.
proof idea
One-line term proof: apply ok_tableOfSubst to the triple (base, base_ok, σ). The general lemma reduces ok-ness of the image to determinant preservation under word evaluation and the inverse-word/adjugate identity, both already established for any ok table. No new algebra is done here.
why it matters
The module doc states that nothing beyond the provenance of the automorphism action is taken on trust, and that the check covers all 48 automorphism images exactly. This lemma is the free closure step: once base is certified ok, every relabelling is ok by computation from the generators, so no additional table is trusted data.
It underwrites the separation strength claim that the gauge group quotiented over has order 96 times free basepoint choice, and that no_gauge_image_of_A_is_B can range over the full automorphism orbit without re-checking homomorphism axioms case by case. Within Recognition Science this is Loom infrastructure for meaning separation, not a forcing-chain (T0–T8) step, but it is the certificate hygiene that makes the depth-two separation witness kernel-checkable.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.