separates_everywhere
plain-language theorem explainer
The finite separation certificate over the recognition-window automorphism set evaluates to true: every listed automorphism distinguishes the two loom witnesses. Anyone citing the gauge-invariant separation of meanings A and B needs this flag. The proof is a pure kernel decision on a closed Boolean computation, not an analytic argument.
Claim. The Boolean certificate $\mathsf{separatesEverywhere}$ equals $\mathsf{true}$. Equivalently, for every automorphism substitution of the recognition window, the chosen invariant of the gauge image of witness configuration $A$ differs from the invariant of witness configuration $B$.
background
The Loom separation module compares two short utterances $A$ and $B$ built from the same codebook and the same multiset of one-bit loop acts. Content $A$ says every door has some key that opens it and one master key locks every door; content $B$ swaps the universal power of the open/lock relations. At depth one (loop-by-loop and abelianised readings) the two are identical, so length or bag-of-edges counting cannot separate them.
Separation is nontrivial only after quotienting by the gauge group of the recognition window: the 48 automorphisms, optional simultaneous loop reversal, basepoint moves, respellings, and reorderings. The module records a Boolean table separatesEverywhere that asserts the chosen invariant differs on every automorphism image of $A$ versus $B$. Downstream theorems turn that table into the statement that no gauge image of $A$ is $B$.
Local setting (module doc): the weaver reproduces the Python-emitted witnesses letter for letter, depth-one readings are blind, and the depth-two/commutator reading differs; the present flag is the exhaustive automorphism half of that package.
proof idea
One-line computational proof: decide. Lean reduces the closed Boolean expression separatesEverywhere = true by evaluating the finite table (automorphism list, invariant comparison) inside the kernel. No lemmas are invoked; the certificate is a pure decision-procedure fact about a fully concrete List.all over the automorphism set.
why it matters
This flag is the computational spine of THE SEPARATION THEOREM no_gauge_image_of_A_is_B: after rewriting by permutation-invariance and gauge-image invariance of the reading, that theorem applies List.all_eq_true.mp separates_everywhere at each automorphism $\sigma$ to conclude the invariants differ, hence no gauge transform of $A$ equals $B$. The same pattern feeds witnesses2_separated for a second witness pair.
In framework terms this is a Loom-level meaning separation, not a forcing-chain step (T5–T8). It shows two quantifier duals that agree on every depth-one carrier and on cost are still distinct meanings under the full recognition-window gauge group (order 96 times basepoint choice, 48 automorphisms checked exactly). The margin is one coordinate in a 21-dimensional finite invariant, the smallest exact gap the institute records for this pair.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.