someKeyEveryDoorLocks
plain-language theorem explainer
Encodes the quantified claim that a single master key locks every door: existential over keys, universal over doors, of the lock relation. Part of the safe half of the Loom separation pair (witness A). Pure expression-tree constructor; no proof obligations.
Claim. The Loom expression $\exists k\,\forall d\,\mathrm{locks}(k,d)$, i.e. there is one key that locks every door.
background
The Loom grammar builds content as finite expression trees over a shared codebook. An Expr is either an atom (a named relation on role fillers, possibly denied), an unordered conjunction, or a quantifier over a shared name; the Boolean flag is true for universal and false for existential.
This module constructs two surface-similar utterances A and B that swap which binary relation (opens vs locks) receives the universal quantifier power. Counting, depth-one loop readings, and abelianised readings cannot separate them; only the depth-two commutator reading and a full gauge sweep do.
Sibling atoms key, door, and locksKeyDoor supply the role names and the lock predicate. The dual open-side formula is the existential-universal pattern on opens.
proof idea
Definitional constructor only. Builds a nested quantifier node: outer existential over the key name, inner universal over the door name, body the locks-key-door atom. No tactics, no lemmas, no reduction.
why it matters
Feeds directly into witnessA, the safe half of the separation pair: every door has some key that opens it, conjoined with one master key that locks every door. Module doc contrasts this with the unsafe dual B (master key opens everything). Together they are the content whose weave, depth-one blindness, abelianised blindness, depth-two separation, and no-gauge-image theorems establish a genuine meaning distinction under a 96-fold gauge quotient, not a length or spelling artifact.
Sits in the Loom domain of Recognition Science: showing that recognition structure can separate security-safe from security-hole readings that cost-identical ground multisets and one-bit act budgets cannot tell apart.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.