everyDoorLocksEveryKey
plain-language theorem explainer
Nested universal quantification asserting that every door locks every key, built as a Loom grammar expression over the shared codebook. Separation and gauge-invariance arguments cite it as one conjunct of witness D. The body is a one-line constructor nesting two universal quantifiers over the locks atom.
Claim. The Loom expression $\forall\,\mathrm{door}\,\forall\,\mathrm{key}\,\mathrm{locks}(\mathrm{door},\mathrm{key})$, where $\mathrm{door}$ and $\mathrm{key}$ are fixed codebook name indices and $\mathrm{locks}$ is the binary relation atom (not denied).
background
The Loom grammar encodes content as finite expression trees: atoms (a predicate index, role-ordered name arguments, and a denial flag), unordered conjunction, and quantifiers over shared names (universal when the flag is true). Names are codebook indices only; nothing is anonymous or claim-local.
In this module the four shared names include door (index 0) and key (index 1). The atom locksDoorKey is the non-denied locks relation on those two roles. The module contrasts two witness pairs that reuse the same ground multiset and the same one-bit act costs, differing only in which relation receives universal force: A is secure (every door has some opening key; one master key locks every door), while B is a security hole (every door has some locking key; one master key opens every door).
Upstream, Expr is the native content type accepted by the language; evaluation and readings act on that tree, never on uncountable graphs.
proof idea
Pure definitional construction, not a proof. The term is the grammar constructor for a universal quantifier over door, whose body is a universal quantifier over key, whose body is the locks atom on [door, key]. No lemmas or tactics are applied.
why it matters
Forms one conjunct of witness D (someDoorOpensEveryKey conjoined with this expression), the B-side security-hole utterance in the separation pair. The module shows that depth-one and abelianised readings are blind to A versus B, while the commutator (depth-two) reading separates them, and that no image of A under the order-48 recognition-window automorphism group (plus basepoint, reversal, respelling, reordering) equals B. This definition supplies the universally forced locks half of that B witness so the weaver, cost, and gauge checks can run on a concrete grammar term rather than opaque data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.