prev_next
plain-language theorem explainer
The theorem shows that the next phase operation undoes the previous phase shift for any element of the 8-phase cycle. Researchers formalizing discrete time evolution in Recognition Science would reference it when checking cycle consistency in the RRF hypotheses. The proof is a one-line simplification that unfolds the definitions of next and prev.
Claim. For every phase $p$ in the finite set of eight phases, next(prev($p$)) = $p$.
background
The module states the 8-tick hypothesis as an explicit claim about observed traces: time and process are discretized into 8-beat cycles, with phases 0-3 forming the LOCK segment for structure formation and phases 4-7 forming the BALANCE segment for equilibration. Phase is introduced as the abbrev Fin 8, the finite set of eight phases in one cycle. Upstream, Tick is the atomic ledger unit of temporal progression with no background manifold, and the constant tick is fixed to 1 in RS-native units, yielding the fundamental octave of eight ticks.
proof idea
The proof is a one-line wrapper that applies the simp tactic to the definitions of next and prev.
why it matters
The result supplies a basic invertibility property inside the Phase namespace of the 8-tick hypothesis class. It supports the discretization of time required by the eight-tick octave in the forcing chain and supplies a consistency check for the lock-balance partition. No downstream theorems are recorded, leaving its use in larger RRF models open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.