phase_0_is_one
plain-language theorem explainer
The phase exponential at the zeroth position in the eight-tick cycle equals one, which supplies the symmetry sign for bosons under particle exchange. Workers on the Recognition Science derivation of spin-statistics or CPT symmetry cite this identity as the base case of the phase group. The result follows from direct expansion of the phase and exponential definitions together with zero-multiplication lemmas and the fact that the complex exponential of zero is one.
Claim. In the eight-tick phase structure the complex factor at index zero satisfies $exp(i · 0 · π/4) = 1$.
background
The EightTick module defines the discrete clock of Recognition Science with phases kπ/4 for k in Fin 8. The phase function returns (k : ℝ) * π / 4 and phaseExp returns the complex exponential exp(i * phase(k)). This encodes the fundamental 8-tick period that generates spin-statistics and CPT symmetries, as stated in the module documentation.
proof idea
The proof unfolds phaseExp and phase, then applies simp with Nat.cast_zero, zero_mul, zero_div, mul_zero, Complex.ofReal_zero and Complex.exp_zero to reduce directly to exp(0) = 1.
why it matters
This supplies the +1 boson sign used in the spin-statistics key theorem, which pairs it with the -1 at phase 4. It is invoked by boson_rotation_phase_pos_one, cpt_composition, exchange_sign_boson and the spin-statistics certificate. The result realizes the identity element of the eight-tick octave and closes the base case for the discrete symmetry group ℤ/8ℤ.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.