locks
plain-language theorem explainer
Natural-number atom code for the binary predicate “locks” in the Loom separation grammar, fixed at index 3 in the search-chosen codebook. Anyone building quantified door/key expressions or reading certificate data cites it. The body is a one-line constant definition with no proof obligations.
Claim. Define the atom index $\mathrm{locks} := 3 \in \mathbb{N}$. In the separation witness language this is the codebook slot for the binary ground relation “locks” on the pair $(\mathrm{door},\mathrm{key})$, in name order $[\mathrm{door},\mathrm{key},\mathrm{opens},\mathrm{locks}]$.
background
The Loom separation module compares two quantified utterances about doors and keys. Content A says every door has some key that opens it and one master key locks every door; content B swaps the universal power onto the opposite relation and is a security hole. Both are built from four ground atoms: door, key, opens, locks.
Those atoms are not strings inside Lean. They are natural indices into a codebook chosen by exhaustive search so that no length statistic separates A from B (the hard case). Certificate data records the chosen codes as the list $[-1,3,4,5]$ in name order door, key, opens, locks. The present definition simply binds the fourth name to its index.
Upstream length and trace machinery (finite-trace length, stable conjunction of trace predicates) is what later readings use when they count one-bit acts; the atom indices themselves stay pure labels until expressions are woven and read.
proof idea
One-line constant definition: the right-hand side is the numeral 3. No tactics, no lemmas, no hypotheses. Downstream constructors such as the atomic expression builder simply substitute this Nat into the atom slot of an Expr.
why it matters
Without a fixed index for “locks”, the quantified separation statements cannot be assembled. Downstream definitions build the locking atoms and the two quantifier patterns that use them: every door has some key that locks it, one master key locks every door, and the swapped door/key atom orders. Certificate data packages the same codebook so the Python encoder and the Lean weaver agree letter for letter.
That agreement is what lets the module prove the nontrivial separation: depth-one and abelianised readings are blind on the pair, the commutator reading differs, and no gauge image of A equals B under the full automorphism action of the recognition window. The constant is scaffolding for those theorems, not a physics claim of its own; it sits in the Loom layer that feeds meaning-separation arguments rather than in the T0–T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.