lock_balance_disjoint
plain-language theorem explainer
The declaration proves that no phase in the 8-tick cycle belongs to both the LOCK and BALANCE regions. Researchers modeling discrete recognition traces cite it to enforce consistent partitioning of the cycle. The proof unfolds the two predicates and invokes a linear-arithmetic decision procedure to obtain the contradiction.
Claim. For every phase $p$ in the 8-element cycle, it is not the case that $p$ satisfies the LOCK predicate ($p.val ≤ 3$) and the BALANCE predicate ($p.val ≥ 4$).
background
The module states the 8-tick hypothesis: observed folding and recognition traces exhibit 8-phase periodicity, with phases 0–3 assigned to LOCK (structure formation) and phases 4–7 assigned to BALANCE (equilibration). Phase is defined as the finite type Fin 8. The predicates isLock and isBalance are the local definitions that realize this partition: isLock holds precisely when the phase index is at most 3, and isBalance holds when the index is at least 4. Upstream results supply the underlying 8-tick phase map (kπ/4 for k = 0 … 7) and the general Phase abbreviation used across the Recognition Science codebase.
proof idea
The term proof first applies simp with the definitions of isLock and isBalance, expanding the goal to the conjunction p.val ≤ 3 ∧ p.val ≥ 4. The omega tactic then derives a contradiction from these incompatible bounds on an integer between 0 and 7.
why it matters
The result secures the internal consistency of the explicit 8-tick discretization hypothesis that the RRF module supplies for testing observed traces. It directly implements the separation between LOCK and BALANCE regions required by the eight-tick octave (T7) in the forcing chain. Because the declaration has no downstream uses yet, it functions as a foundational consistency lemma for any later development that relies on the partitioned cycle.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.