opens
plain-language theorem explainer
Assigns the natural-number token index 2 to the binary relation “opens” in the Loom separation vocabulary (door, key, opens, locks). Downstream certificate configs and separation lemmas cite this constant so that ground atoms and codebook entries stay aligned with the Python encoder. The body is a one-line numeric definition.
Claim. The vocabulary index for the relation “opens” is the natural number $2$ (third slot in the ordered list door, key, opens, locks).
background
The Loom separation module compares two quantified statements about doors and keys that share the same multiset of ground facts and the same one-bit act costs, yet differ in meaning. The four atomic names are indexed in fixed order: door, key, opens, locks. Configurations and codebooks are lists of integers that refer to these indices (and their sign-flipped duals).
Module documentation frames the pair as: (A) every door has some key that opens it, and one master key locks every door; versus (B) the security-hole dual with the universal power swapped. Counting and depth-one readings are blind to the pair; only a depth-two (commutator) reading and a full gauge check separate them.
Certificate data records the blinding-search codebook in exactly this name order, so the constant here is the stable handle for the opens atom inside those lists.
proof idea
Pure definition: the identifier is bound to the numeral 2. No proof obligations, lemmas, or tactics.
why it matters
Gives a single named index for the opens relation so certificate configs (cfgA, cfgC), codebooks (cbData, cbData2), and separation predicates (opensKeyDoor, locksKeyDoor, everyDoorSomeKeyOpens) stay synchronized with the encoder. Without a fixed index, the exhaustive automorphism and basepoint checks that prove no gauge image of A is B would be ill-typed against the grammar. The constant is scaffolding for the kernel-checked separation witness, not a physics claim itself; cosmology and cost-ladder uses appear only as incidental name reuse of the integer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.