phase_0_is_one
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.
claimIn 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 in Recognition Science
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ℤ.
scope and limits
- Does not evaluate the phase exponential at nonzero indices.
- Does not establish the eighth-power identity for the full cycle.
- Does not derive CPT invariance without further composition steps.
- Does not connect to continuous spacetime limits.
Lean usage
example : phaseExp ⟨0, by norm_num⟩ = 1 := phase_0_is_oneformal statement (Lean)
76theorem phase_0_is_one : phaseExp ⟨0, by norm_num⟩ = 1 := by
proof body
Term-mode proof.
77 unfold phaseExp phase
78 simp only [Nat.cast_zero, zero_mul, zero_div, mul_zero, Complex.ofReal_zero,
79 Complex.exp_zero]
80
81/-- The fundamental frequency associated with the 8-tick. -/