next
plain-language theorem explainer
Defines the cyclic successor operation on phases within the 8-beat discretization. Researchers modeling periodic traces in Recognition Science cite it when advancing through LOCK and BALANCE segments of the cycle. The implementation is a direct one-line assignment that increments the underlying Fin 8 element.
Claim. Let $p$ belong to the cyclic phase set $P = Fin 8 = {0,1,2,3,4,5,6,7}$. The successor function satisfies $next(p) = p + 1$ (modulo 8).
background
The module encodes the explicit hypothesis that 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 introduced as the finite type Fin 8. Upstream results supply the angular realization: Foundation.EightTick.phase maps each index k in Fin 8 to kπ/4, while ChurchTuringPhysicsStructure.Phase and RiemannHypothesis.Wedge.phase reuse the identical Fin 8 carrier for information-theoretic and complex-phase contexts.
proof idea
One-line definition that applies the built-in addition operation on Fin 8, which automatically performs the required modular reduction.
why it matters
It supplies the successor needed to realize the eight-tick octave (T7) of the forcing chain and is invoked by forty downstream results, including bimodal_ratio_gt_thirty in PulsarPeriodFromRung and normalizedRadius together with ionization_monotone_within_period in the chemistry modules. The module documentation presents the construction as the testing interface for the 8-tick hypothesis, leaving open the falsification route via observed traces that prefer a different cycle length.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.