witnessD_fails
plain-language theorem explainer
Under the fixed witness model, the formula called witness D evaluates to false at the zero assignment. Anyone checking that the second rival quantified claim is not realized by the intended door-key model cites this. The proof is a one-line kernel decision: the finite Boolean expression is closed by `decide`.
Claim. Evaluating the witness-$D$ expression in the witness model, with every free variable assigned the value $0$, yields false.
background
The Loom separation module contrasts two quantified door-key stories that share the same multiset of ground facts and the same binder pattern, and therefore look identical to any depth-one or abelianised reading. Content A says every door has some key that opens it, and one master key locks every door. Content B (the security hole) swaps the roles of the two relations under the same quantifier shapes.
Witness formulas are built from the atomic relations opens and locks on doors and keys, then evaluated by evalExpr against a concrete finite model (witnessModel). The zero environment fun _ => 0 is the default ground assignment used for closed Boolean checks. The module's point is that counting and length multisets cannot separate the rivals; only a deeper (commutator / gauge-invariant) reading can.
Upstream Loom imports supply the grammar, readings, semantics, and certificate data that define how these expressions are woven and scored. The present lemma is the model-side failure fact for the D side of a second witness pair.
proof idea
Term-mode proof discharged entirely by decide. After unfolding the concrete finite model, the expression, and the constant-zero environment, the goal is a closed Boolean equality, which the kernel decides by exhaustive evaluation. No lemmas are invoked by name.
why it matters
This is the model-failure half of the second separation pair. Downstream, witnesses2_separated uses the woven forms of witnesses C and D together with the gauge-image non-equality machinery: for every automorphism substitution in the recognition-window gauge group, every basepoint move, and optional reversal, no gauge image of the C weave equals the D weave. Establishing that D itself fails in the intended model pins that D is not an accidental true twin of a satisfied formula; it is a genuine rival meaning.
In the module's terms, the separation is nontrivial precisely because depth-one and abelianised readings are blind on the pair, while the commutator reading and the full order-96 gauge quotient (48 automorphisms, basepoint, reversal) still keep A/C apart from B/D. The lemma is a small but necessary Boolean anchor in that chain: without model failure of D, the weave-level non-identity would not certify distinct meanings.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.