phase_wraps_24
plain-language theorem explainer
The theorem proves periodicity of the diurnal phase function with period 24 for any natural number h. Climate modelers applying the Recognition Science eight-tick structure to daily cycles would cite this to close the wrapping property. The proof is a direct one-line wrapper that unfolds the modulo-8 definition and applies an arithmetic solver.
Claim. For every natural number $h$, the diurnal phase satisfies $diurnal_phase(h + 24) = diurnal_phase(h)$, where $diurnal_phase(h) := h mod 8$.
background
The module derives the 24-hour climate cycle from the universal 8-tick cadence forced by three spatial dimensions, with the diurnal phase defined as the hour reduced modulo 8. This yields eight distinct phases at 3-hour granularity, consistent with the octave period in the Recognition Science framework. Upstream, the EightTick.phase definition supplies the angles $kπ/4$ for $k = 0$ to $7$, while the tick constant fixes the fundamental RS-native time quantum.
proof idea
The proof is a one-line wrapper that unfolds the definition of diurnal_phase, reducing the claim to the arithmetic identity $(h + 24) mod 8 = h mod 8$. The omega tactic then discharges the fact that 24 is a multiple of 8.
why it matters
This supplies the periodicity clause required by the master theorem diurnal_master and the certificate DiurnalEightTickCert. It directly instantiates the eight-tick octave (T7) for the climate domain, confirming that the diurnal cycle inherits the $2^D = 8$ structure with $D = 3$. The result completes the discrete wrapping needed for the full 8-phase partition without introducing new hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.