separatesEverywhere
plain-language theorem explainer
Boolean certificate that the Loom invariant of configuration A differs from that of B under every one of the forty-eight automorphisms of the recognition window. Anyone citing the Loom gauge-quotient separation uses it as the decidable witness behind the separation theorem. It is a pure definition: a universal fold of inequality checks over the trusted automorphism list.
Claim. The Boolean that is true precisely when, for every automorphism $\sigma$ among the forty-eight relabellings of the recognition window, the Loom invariant of configuration $A$ on the $\sigma$-substituted base table differs from the Loom invariant of configuration $B$ on the unsubstituted base table.
background
The Loom separation module contrasts two door-key statements that share the same multiset of ground facts and the same one-bit act costs and per-loop length multiset, so counting cannot tell them apart. Configuration $A$ says every door has some key that opens it and one master key locks every door; configuration $B$ swaps the universal quantifier onto the opening relation (a security hole). Depth-one and abelianised readings are identical on the pair; only a deeper invariant separates them.
The gauge action under study includes the forty-eight automorphisms of $Q_3$ on five free generators. That list (autSubst) is the sole trusted external datum; everything else the separation needs is computed inside Lean. The base table is the homomorphism found by search; the invariant lands in a finite set with twenty-one coordinates.
Upstream, the TraceLogic universal fold packages a family of stable finite-trace predicates into one predicate. Here it is used only as the Boolean all over the automorphism list.
proof idea
Not a proof: a two-line Boolean definition. It folds all over the forty-eight substitutions in autSubst, and at each $\sigma$ checks that the invariant of $A$ on the $\sigma$-substituted base table is unequal to the invariant of $B$ on the unsubstituted base. The result is the conjunction of those inequalities, ready for kernel decision.
why it matters
Feeds the sibling theorem separates_everywhere, which decides the Boolean equals true and is billed as THE SEPARATION THEOREM: no gauge image of $A$ is $B$ (not by any of the forty-eight automorphisms, nor by the broader gauge moves the module treats elsewhere). That is the nontriviality claim of the module: $A$ and $B$ are two meanings, not two spellings of one, while every depth-one carrier conflates them. The margin is exact and minimal (one coordinate of twenty-one). In Recognition terms this is a Loom-level witness that meaning survives the gauge quotient and is invisible to abelianised or length data alone.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.