nextPhase
plain-language theorem explainer
The nextPhase definition advances the discrete phase index by one step inside the cyclic 8-tick clock. Workers modeling spin-statistics, CPT evolution, or discrete gauge dynamics cite it to step the label k forward while staying inside Fin 8. The implementation is a direct modular-arithmetic construction that reduces the successor modulo 8 and supplies the bound proof by norm_num.
Claim. For each index $k$ in the cyclic group of order 8, nextPhase$(k)$ returns the successor index $(k+1) mod 8$.
background
The EightTick module supplies the fundamental discrete clock of Recognition Science: an 8-phase cycle whose angles are $0, π/4, π/2, …, 7π/4$. The sibling phase definition maps each Fin 8 index $k$ to the real angle $k π / 4$, and the module states that this cycle underlies spin-statistics (odd/even phase selects fermion/boson), CPT symmetry, and gauge-group structure. Upstream structures from NucleosynthesisTiers, LedgerFactorization, PhiForcingDerived, SpectralEmergence, and PhysicsComplexityStructure embed the 8-tick dynamics inside J-cost minimization and the discrete φ-tier hierarchy.
proof idea
The definition is a one-line wrapper: it extracts the numeric value of the input Fin 8 element, adds 1, reduces the sum modulo 8, and packages the result back into Fin 8 together with the explicit bound proof supplied by norm_num.
why it matters
nextPhase realizes the elementary advance operation required by the eight-tick octave (T7) in the forcing chain. It supplies the successor map that sibling definitions such as phase_periodic and eight_tick_generates_Z8 rely upon to establish periodicity and the Z8 group structure. The definition therefore closes the discrete-time step inside the Recognition Science clock without introducing continuous parameters or external constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.