lock_balance_partition
plain-language theorem explainer
Every phase in the eight-element cycle belongs to either the LOCK interval (values 0 through 3) or the BALANCE interval (values 4 through 7). Workers on recognition trace discretization cite this partition to confirm that the two regions cover the full cycle without overlap. The argument proceeds by unfolding the two predicate definitions and resolving the resulting integer disjunction with arithmetic tactics.
Claim. For every phase $p$ in the finite set $Fin 8$, either $p.val ≤ 3$ or $p.val ≥ 4$.
background
The module formalizes the 8-tick hypothesis that observed folding and recognition traces exhibit 8-phase periodicity, with phases 0-3 dedicated to LOCK (structure formation) and phases 4-7 to BALANCE (equilibration). Phase is the type Fin 8. The predicates isLock and isBalance are defined by direct comparison of the phase value against the thresholds 3 and 4 respectively.
proof idea
The term proof first applies simp to replace isLock and isBalance by their defining inequalities, then invokes omega to discharge the resulting arithmetic statement that any integer between 0 and 7 satisfies at least one of the two bounds.
why it matters
This theorem supplies the partition property required by the 8-tick discretization hypothesis in the RRF layer. It directly implements the statement that LOCK and BALANCE together exhaust the cycle, as described in the module documentation. The result anchors the testing interface for LNAL bytecode cycles and connects to the broader forcing chain through the eight-tick octave (T7).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.