separatesEverywhere2
plain-language theorem explainer
Boolean certificate that every automorphism image of the base table, read on configuration C, yields a loom invariant different from the base table on configuration D. Cited by the second separation theorem, which asserts the flag equals true. Pure computational fold over the trusted 48-element automorphism list; no proof content beyond the definition.
Claim. The Boolean that holds if and only if, for every automorphism substitution $\sigma$ of the recognition window, the loom invariant of the $\sigma$-substituted base table on configuration $C$ differs from the loom invariant of the unsubstituted base table on configuration $D$.
background
The Loom separation module compares two short utterances that every depth-one or abelianised reading conflates, yet that no gauge move identifies. Configurations $C$ and $D$ are the two concrete loop lists: $C$ encodes "some door is opened by every key, and every door opens every key"; $D$ encodes the dual security-hole pattern. The base table is the homomorphism found by exhaustive search; tableOfSubst applies an automorphism word-substitution to it.
The only trusted external datum is autSubst, the action of the forty-eight automorphisms of $Q_3$ on the five free generators (as words). Everything else the separation needs is computed inside Lean from that list. The loom invariant is a 21-coordinate finite-set reading of a table against a configuration; equality of invariants is exact, not approximate.
Module setting: two contents that share the same multiset of ground facts and the same one-bit act cost, so counting cannot separate them. Separation is nontrivial precisely because depth-one and abelianised carriers are blind on the pair.
proof idea
Definition, not a proof. It is the Boolean fold autSubst.all of the pointwise test that invariant (tableOfSubst base σ) cfgC is unequal to invariant base cfgD. The universal quantifier is the TraceLogic all combinator over the finite automorphism list; evaluation is pure computation on certificate data.
why it matters
Feeds the theorem separates_everywhere2, which decides the flag equals true and is described as "THE SECOND SEPARATION THEOREM, and the strongest statement in this file": two pieces of content that every local-fact reading identifies, and that no gauge transformation of the utterance identifies. Together with the first separation (no gauge image of A is B) it closes the module claim that the gauge group of order 96 (times free basepoint choice) never maps one meaning onto the other, while the invariants differ in exactly one of twenty-one coordinates, the smallest possible exact margin.
In the broader Loom story this is the computational witness that meaning is not recoverable from length multisets or depth-one carriers; the commutator (depth-two) reading is required. It does not itself touch the T0–T8 forcing chain, but it is the kernel-checked certificate that the recognition grammar distinguishes dual quantifier patterns the codebook was deliberately built to cost-equate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.