noon_phase
plain-language theorem explainer
The theorem shows that the diurnal phase at hour 12 equals 4. Climate researchers working with quantized 24-hour cycles cite this when confirming solar noon sits at the midpoint of the eight-phase structure. The proof is a one-line wrapper that unfolds the modular definition and applies reflexivity.
Claim. Let $d(h) := h mod 8$ be the diurnal phase at hour $h$. Then $d(12) = 4$.
background
The module shows that the 24-hour diurnal cycle inherits the universal 8-tick cadence forced by three spatial dimensions, since $2^3 = 8$. The diurnal phase is defined as the remainder when the hour is divided by 8, mapping the day into eight equal 3-hour segments. Upstream results include the general phase definition in the EightTick foundation, which assigns phases $k pi / 4$ for $k = 0$ to $7$, and the complex phase in the Riemann Hypothesis wedge.
proof idea
The proof is a one-line wrapper that unfolds the definition of diurnal_phase as $h % 8$ and applies reflexivity to obtain 12 mod 8 = 4.
why it matters
This supplies the noon_at_4 field of DiurnalEightTickCert and is invoked in the master theorem diurnal_master, which asserts the full 8-phase partition with noon at phase 4 and 24-hour periodicity. It instantiates the T7 eight-tick octave landmark in the climate domain, confirming alignment with the forced 8-fold structure from D = 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.