phase
plain-language theorem explainer
The phase definition maps each index k in Fin 8 to the angle kπ/4, supplying the discrete phases of the Recognition Science clock. Modelers of spin-statistics, CPT symmetry, or diurnal cycles cite this when discretizing time evolution on the eight-tick octave. It is a direct arithmetic definition with no lemmas or reductions required.
Claim. For each $k$ with $0 ≤ k ≤ 7$, the phase angle is given by $k π / 4$.
background
The EightTick module sets out the fundamental discrete clock of Recognition Science. Its phases are listed explicitly as 0, π/4, π/2, 3π/4, π, 5π/4, 3π/2, 7π/4. This structure is stated to underlie spin-statistics (odd/even phase to fermion/boson), CPT symmetry, gauge groups, and quantum phase accumulation. The upstream tick definition supplies the fundamental time quantum τ₀ = 1 in RS-native units, with one octave defined as exactly eight ticks.
proof idea
The declaration is a direct definition that scales the Fin 8 index by π/4 using ordinary real arithmetic; no lemmas are invoked.
why it matters
This definition realizes the eight-tick octave (T7) that generates Z8 symmetry and supplies the phase values used by downstream declarations such as diurnal_phase, noon_phase, and the nucleosynthesis tiers structure. It closes the discrete-time foundation needed for the forcing chain and for the spin-statistics key that appears in the same module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.