everyDoorSomeKeyLocks
plain-language theorem explainer
Encodes the quantified claim that every door has some key locking it, as a Loom grammar expression over shared codebook indices. Separation and witness constructions cite it as one conjunct of the unsafe pair B. The body is a pure term: universal over door, existential over key, applied to the locks atom.
Claim. The Loom expression $\forall\,\mathrm{door}\,\exists\,\mathrm{key}\,\mathrm{locks}(\mathrm{key},\mathrm{door})$, with door, key, and locks as fixed codebook indices and the atom un-denied.
background
The Loom separation module compares two quantified utterances that share the same multiset of ground facts and the same one-bit act costs, yet differ in meaning. Content A is safe (every door has a key that opens it, and one master key locks every door); content B is the security hole (every door has a key that locks it, and one master key opens every door). They swap which relation receives universal power.
Expressions live in the Loom grammar: atoms name a predicate and role fillers by codebook index, optionally denied; quantifiers bind a shared name, universal when the flag is true. Here door, key, and locks are the indices 0, 1, and 3. The atom locksKeyDoor is locks applied to [key, door] without denial. Nested quantifiers over those names build the quantified claim.
proof idea
One-line definitional term. It wraps locksKeyDoor in an existential quantifier over the key index, then a universal quantifier over the door index (flag true for universal, false for existential). No lemmas or tactics; the expression tree is the object.
why it matters
This is the first conjunct of witnessB, the unsafe separation witness: every door has some locking key, conjoined with one master key that opens every door. The module shows that depth-one and abelianised readings are blind to the A/B pair, while the commutator (depth-two) reading separates them, and no gauge image of A equals B across the full automorphism group of the recognition window. The definition supplies the quantified half that makes B the security hole rather than a restatement of A, so counting and length statistics cannot tell the pair apart.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.