someDoorLocksEveryKey
plain-language theorem explainer
Encodes the first-order sentence “there exists a door that locks every key” as a Loom grammar expression tree. Separation and witness constructions cite it as one conjunct of a composite content term. The body is a pure constructor term: existential over the door name, then universal over the key name, applied to the locks atom.
Claim. The Loom expression $\exists\,\mathrm{door}\,\forall\,\mathrm{key}\,\mathrm{locks}(\mathrm{door},\mathrm{key})$, built as nested quantifiers over the shared codebook indices for door and key, with the positive locks atom as matrix.
background
The Loom separation module compares two short first-order contents that share the same multiset of ground facts and the same one-bit act cost, yet differ in which binary relation receives universal force. Content is written in Grammar.Expr: atoms name a codebook predicate and role fillers; quantifiers bind shared name indices, with a Boolean flag true for universal and false for existential.
Local names are fixed codebook indices: door $= 0$, key $= 1$, and the locks predicate is the atom on those two roles (not denied). The sibling locksDoorKey is exactly that atom. The module’s point is that counting and depth-one readings cannot separate two such patterns, while a depth-two commutator reading and a full gauge sweep can.
Upstream, Expr is the finite expression tree the weaver and readings consume; nothing anonymous is ever named, only indices into the shared codebook.
proof idea
One-line definitional constructor. It builds .quant false door (existential over the door index) whose body is .quant true key locksDoorKey (universal over the key index of the locks atom). No lemmas or tactics; the term is the claim.
why it matters
Feeds witnessC, the conjunction of this sentence with “every door opens every key.” That composite is part of the module’s family of separation witnesses used to show that two contents can agree on loop-by-loop and abelianised readings yet differ under the commutator reading, and that no gauge image of one equals the other.
In the module’s terms, the security-hole pattern (universal power on the wrong relation) is distinguished from the safe pattern only after depth two and after quotienting by the full automorphism action of the recognition window. This definition supplies one quantified half of that content pair in grammar-native form, so later weave and blindness theorems talk about the grammar rather than opaque encoder output.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.