isLock
plain-language theorem explainer
The isLock definition flags phases 0-3 as the LOCK region inside the 8-phase cycle. Modelers of discretized recognition traces cite it to separate structure-formation intervals from equilibration intervals. It is realized by a direct numerical comparison on the Fin 8 representative.
Claim. Let $p$ be a phase in the 8-beat cycle, i.e., an element of the finite set $0,1,2,3,4,5,6,7$. Then isLock$(p)$ holds precisely when the integer representative of $p$ satisfies $p.val ≤ 3$.
background
The RRF.Hypotheses.EightTick module encodes the explicit 8-tick hypothesis that observed folding and recognition traces are periodic with period 8. Phase is introduced as the abbreviation Fin 8, with the convention that indices 0-3 label the LOCK region (structure formation) and 4-7 label the BALANCE region (equilibration). This local convention is stated directly in the module documentation: “Phase 0-3: LOCK (structure formation) Phase 4-7: BALANCE (equilibration).”
proof idea
The declaration is a one-line definition that evaluates the Boolean p.val ≤ 3 on the underlying integer of the Fin 8 type. No lemmas or tactics are invoked; the predicate is obtained by direct projection onto the representative.
why it matters
isLock supplies the indicator used by the sibling theorems lock_balance_partition and lock_balance_disjoint, which together establish that the eight phases form a clean partition into LOCK and BALANCE sets. The definition therefore realizes the 8-tick discretization hypothesis (T7 eight-tick octave) inside the Recognition Science forcing chain and is referenced by the LockPhasePrediction structure that demands higher structural change precisely during LOCK phases.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.