someDoorOpensEveryKey
plain-language theorem explainer
Defines the Loom expression for “some door opens every key”: an existential over the door role and a universal over the key role applied to the opens atom. Separation and witness constructions cite it as one conjunct of witness D. The body is a one-line nested quantifier tree in the shared Expr grammar, not a proved claim.
Claim. The content expression $\exists\,\mathrm{door}\,\forall\,\mathrm{key}\,\mathrm{opens}(\mathrm{door},\mathrm{key})$, built as nested quantifiers over the shared codebook names for door, key, and the opens relation (not denied).
background
The Loom separation module compares two short quantified claims about doors and keys that agree on shallow readings and on bit-cost multisets, yet differ under a depth-two commutator reading and under the full gauge orbit of the recognition window. Content is written in Grammar.Expr: atoms name a predicate and role fillers by codebook index, and quantifiers bind a shared name with a universal/existential flag.
Here the four names are fixed indices: door $= 0$, key $= 1$, opens $= 2$. The ground atom opensDoorKey is the non-denied opens relation on those two roles. Nested quantifiers then package the classical pattern “there is a door that opens every key.” The module’s point is that counting and depth-one carriers cannot tell this family of patterns apart from its dual security-hole twin; only deeper structure and gauge-invariant readings separate them.
proof idea
Pure definitional construction, not a proof. The term is .quant false door (.quant true key opensDoorKey): outer existential on the door name, inner universal on the key name, body the opens atom on [door, key]. No lemmas or tactics fire; the Expr inductive from the Loom grammar supplies the constructors.
why it matters
Feeds witnessD, the conjunction of this formula with “every door locks every key.” That witness is one of the two content packages the module uses to stage the separation: same quantifier shapes and same ground multiset cost as its twin, yet not gauge-equivalent under the forty-eight window automorphisms, basepoint moves, reversals, respellings, or loop reorderings. The parent story is the kernel-checked claim that depth-one and abelianised readings are blind while the commutator reading and the full gauge check separate the pair. This def is the first conjunct that makes witness D a concrete, letter-for-letter weavable utterance rather than an informal English claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.