witnessD
plain-language theorem explainer
Defines the second separation witness as the conjunction of “some door opens every key” with “every door locks every key.” Separation and blindness theorems cite it as the security-hole claim paired against witness C. The body is a one-line constructor application building a grammar expression tree.
Claim. Let $D$ be the loom expression $\bigl(\exists\,\mathrm{door}\,\forall\,\mathrm{key}\,\mathrm{opens}\bigr)\land\bigl(\forall\,\mathrm{door}\,\forall\,\mathrm{key}\,\mathrm{locks}\bigr)$, i.e. the unordered conjunction of the existential–universal open claim with the fully universal lock claim.
background
The Loom separation module builds two short quantified claims that share the same ground multiset, the same adjacency bag, and the same one-bit cost profile, yet mean different things under a plain two-element model. Content is an Expr tree from the loom grammar: atoms name codebook predicates and role fillers, conj is unordered conjunction, and quantifiers bind shared names (universal when the flag is true).
The two conjuncts here are already named. “Some door opens every key” is the existential–universal open formula; “every door locks every key” is the double universal lock formula. Their conjunction is the security-hole side of the pair: one master door opens every key, and locking holds universally. The module’s other witness swaps which relation carries the universal power, so counting and depth-one readings cannot tell the two apart.
proof idea
Pure definition: apply the grammar constructor conj to the two already-defined subexpressions someDoorOpensEveryKey and everyDoorLocksEveryKey. No proof obligations, no tactics.
why it matters
This is one pole of the kernel-checked separation pair. Downstream, weave_witnessD shows the weaver reproduces the Python encoder’s utterance letter for letter; wellFormed_D discharges well-formedness via that weave; witnessC_ne_witnessD records that the trees differ; and witnessC_and_D_are_different_claims plus witnessD_fails show that on the plain two-element model C holds and D fails.
Blindness results groundBag_blind and adjacencyBag_blind prove that ground multisets and parent–child label pairs are permutations of those of witness C, so rivals that stop at bags of facts or local parse labels cannot separate them. The module then lifts the distinction through depth-two commutator readings and a full check that no gauge image of one is the other. In Recognition terms this is a meaning-level separation under a large gauge quotient, not a length or cost artifact.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.