key
plain-language theorem explainer
The constant key is the natural number 1, serving as a concrete key label in the Loom separation witness. It is the carrier for the existential and universal key quantifiers in the open/lock door relations that distinguish utterances A and B. Anyone citing the separation grammar or the witness constructions uses this value. The declaration is a bare numeric definition with no proof obligations.
Claim. Define the distinguished key label by $\mathrm{key} := 1 \in \mathbb{N}$.
background
The Loom.Separation module formalizes a separation witness for two utterances that counting and depth-one readings cannot tell apart. Content A asserts that every door has some key that opens it and one master key locks every door; content B swaps the relations so every door has some key that locks it and one master key opens every door. B is a security hole; A is not. Both use the same quantifier patterns over the same two binary relations on doors and keys.
Keys and doors are coded as natural numbers. The sibling constants and predicates (door, opens, locks, and the quantified packages everyDoorSomeKeyOpens, someKeyEveryDoorLocks, and so on) build the ground facts that the weaver and the depth-two commutator reading later separate. The module proves the two weaves match the encoder output letter for letter, that depth-one and abelianised readings are blind to the pair, that the commutator reading differs, and that no gauge image of A equals B.
proof idea
Bare definition: the identifier is bound to the natural-number literal 1. No tactics, no lemmas, no reduction.
why it matters
Without a fixed key label the open/lock ground facts and the quantified witness packages cannot be stated. This constant is the concrete witness value threaded through opensKeyDoor, locksKeyDoor, everyDoorSomeKeyOpens, someKeyEveryDoorOpens, everyDoorSomeKeyLocks, someKeyEveryDoorLocks, and the top-level separation theorems weave_witnessA, weave_witnessB, depth_one_is_blind, depth_two_separates, and no_gauge_image_of_A_is_B.
In the broader Recognition framework the separation shows that two meanings with identical one-bit act counts and identical per-loop length multisets are still distinct once the commutator (depth-two) reading and the full gauge orbit (order 96 times basepoint choice, 48 automorphisms checked exactly) are admitted. The margin is one coordinate in a twenty-one-dimensional finite invariant, the smallest possible exact gap. Downstream consumers across Action, Constants, and Cosmology inherit the Loom vocabulary; this definition is the atomic key tag those graphs rely on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.