separates_everywhere2
plain-language theorem explainer
A closed Boolean certificate that the second loom witness pair is separated under every recognition-window automorphism. Downstream separation theorems cite it to discharge the exhaustive gauge check. The proof is a one-line kernel decision on a fully concrete Boolean term.
Claim. The precomputed Boolean flag that records, for every automorphism of the recognition window, that the second pair of loom configurations is separated, evaluates to $\mathsf{true}$.
background
The Loom separation module studies two pairs of utterances that assert the same two relations under the same quantifier patterns and differ only in which relation carries universal force. A multiset of ground facts and a cost-matched codebook therefore cannot tell the members of a pair apart: depth-one (loop-by-loop) and abelianised readings are identical on each pair, so any carrier that stops at depth one conflates them.
Separation becomes nontrivial only at depth two (the commutator reading) and under the full gauge action: the 48 automorphisms of the recognition window, basepoint moves, optional reversal, respelling, and loop reordering. The module already shows the weaver reproduces the encoder output letter-for-letter, so everything below is about the grammar, not opaque data.
separatesEverywhere2 is the finite Boolean that packages the exhaustive second-pair check over that automorphism set. Its value is what the kernel decides here.
proof idea
One-line computational proof: decide evaluates the closed term separatesEverywhere2 in the kernel and confirms it equals true. No lemmas are applied; the certificate is a concrete Boolean (typically a List.all over the automorphism list comparing invariants), so decision procedure suffices.
why it matters
This is the computational spine of the second separation theorem, called in the file the strongest statement present. no_gauge_image_of_C_is_D rewrites a permuted gauge image to the invariant, then uses List.all_eq_true.mp separates_everywhere2 to obtain inequality of invariants for every automorphism, flip, basepoint word, and configuration. witnesses2_separated routes through that result to conclude no gauge image of the woven C-witness equals the woven D-witness.
In framework terms the check quotients by a gauge group of order 96 times free basepoint choice, covers all 48 automorphism images exactly, and records an exact one-coordinate disagreement in a 21-dimensional finite invariant, the smallest possible margin. That is the institute-grade strength claim for meaning separation beyond counting or depth-one readings.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.