witnesses_separated
plain-language theorem explainer
Any gauge image of the woven utterance for formula A (every door has a key that opens it; one master key locks all) is never equal, even up to loop reordering, to the woven utterance for formula B (the swapped security-hole reading). Separation theorists and Loom semantics users cite this as the content-level non-identification under the full gauge group. The proof rewrites the two weaves to their concrete configs and applies the exhaustive no-gauge-image lemma.
Claim. For every automorphism substitution $\sigma$ of the recognition window, every basepoint word $g$, every optional global reversal, and every configuration $c$ merely a permutation of the gauge image of the woven utterance of witness A under that data, one has $c \neq$ the woven utterance of witness B.
background
The Loom separation module fixes two first-order contents that assert the same two binary relations under the same two quantifier patterns and differ only in which relation receives universal force:
- A: every door has some key that opens it, and one master key locks every door;
- B: every door has some key that locks it, and one master key opens every door.
B is a security hole; A is not. A codebook was chosen by exhaustive search so both utterances cost the same number of one-bit acts with the same per-loop length multiset, and every depth-one (loop-by-loop or abelianised) reading agrees on the pair. The nontrivial claim is therefore semantic, not metric.
Gauge moves include the 48 automorphisms of the recognition window, basepoint change, optional simultaneous reversal, respelling, and loop reordering. The module already records that the Lean weaver reproduces the Python-emitted strings letter-for-letter (weave_witnessA, weave_witnessB), so the comparison is about the grammar, not opaque data. Upstream cost and dimension constants (J-cost, $D=3$) sit in the broader RS stack but are not invoked in this particular proof.
proof idea
Short tactic proof. Rewrite the hypothesis with weave_witnessA so the gauge image is taken of the concrete woven config of A rather than the abstract witness. Rewrite the goal with weave_witnessB so the right-hand side is the concrete woven config of B. Discharge by gauge_image_ne_B, the exhaustive lemma that no gauge image of A equals B under any automorphism in autSubst, any flip, any basepoint word, and any loop permutation.
why it matters
This is the flagship content-level separation packaged as a single statement: the two formulas receive utterances that no gauge transformation identifies, even though every depth-one reading agrees (module claim no_gauge_image_of_A_is_B, restated for configs). It sits inside the Loom domain's answer to whether recognition semantics can distinguish meanings that counting, act totals, and abelianised readings conflate.
Downstream, witnesses2_separated copies the same shape for the second witness pair (C/D), which is separated under every codebook while act count and amplitude separate it under none. Together they show the gauge quotient (order 96 times free basepoint choice, all 48 automorphisms checked) does not collapse relational content that depth-one carriers cannot see. The margin is exact and minimal: the invariants differ in one coordinate of twenty-one. Framework landmarks T7 (eight-tick) and the recognition window enter only as the ambient automorphism group being quotiented; the result itself is a pure Loom semantics theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.