witnesses2_separated
plain-language theorem explainer
No gauge image of the woven second certificate (witness C) can equal the woven witness D, for any recognition-window automorphism, flip, respelling, or loop reordering. Separation auditors for the Loom C/D pair cite this as the final non-equality under the full gauge action. The proof rewrites both weaves to concrete forms and applies the exhaustive gauge-image non-equality lemma.
Claim. Let $\sigma$ be a substitution in the recognition-window automorphism table, $\mathrm{flip}$ a Boolean basepoint flip, $g$ a respelling word, and $c$ a configuration. If $c$ is a permutation of the gauge image of the weave of witness $C$ under $(\sigma,\mathrm{flip},g)$ with codebook $\mathrm{cb}_2$, then $c$ is not equal to the weave of witness $D$.
background
The Loom separation module compares two quantified claims that share the same multiset of ground facts and the same one-bit act cost profile, so length counting and depth-one loop readings cannot tell them apart. Pair A/B is the secure pattern (every door has some key that opens it; one master key locks every door). Pair C/D is the dual security-hole pattern under swapped quantifier power on the open/lock relations.
A configuration here is a multiset of woven loops produced by the grammar weaver from a certificate word and a fixed codebook. The gauge action combines one of the 48 window automorphisms, an optional simultaneous reversal, a free basepoint word, and loop reordering (permutation). The module already shows the weaver reproduces the encoder output letter-for-letter for both witnesses, that depth-one and abelianised readings are blind on the pair, and that the depth-two commutator reading separates them.
The local claim is the C/D analogue of the A/B gauge separation: after quotienting by that full gauge group, the two weaves remain distinct meanings rather than two spellings of one utterance.
proof idea
Short tactic proof. Rewrite the hypothesis with the concrete expansion of the weave of witness C, rewrite the goal with the concrete expansion of the weave of witness D, then apply the already-proved lemma that no gauge image of C equals D (for any automorphism in the table, flip bit, respelling word, and any permutation of the resulting configuration). No new case split or search occurs here; the work sits in that upstream non-equality.
why it matters
Closes the gauge-quotient step for the second certificate pair in the Loom separation story. Together with the depth-two separation and the blindness results for ground and adjacency bag readings, it shows C and D are distinct meanings under a gauge group of order 96 times free basepoint choice, with the invariant differing in one coordinate of twenty-one (exact, not tolerance). That is the institute-strength form of separation: counting and depth-one carriers conflate the pair; the commutator reading and the full automorphism check do not.
No downstream consumers are wired yet in the graph. The module text flags a separate open conjecture linking nontrivial free-group loops to Ken's recognize_ne_defeq judgment; this theorem does not address that gap. Framework-wise it sits in the Loom certificate layer rather than the T0–T8 forcing chain, but it uses the same recognition-window automorphism provenance the monolith treats as trusted input.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.