phase_4_is_minus_one
plain-language theorem explainer
The theorem establishes that the complex phase factor at the fourth tick of the eight-tick cycle equals negative one. This supplies the antisymmetry sign for fermions under particle exchange. Researchers deriving spin-statistics from discrete time structures would cite it as the direct foundation link. The proof reduces the claim to the standard identity exp(i pi) equals negative one after unfolding the phase definitions and applying ring simplification.
Claim. For the phase function defined by $k$ times pi over 4 with $k$ in the finite set of eight ticks, the complex exponential at the fourth tick satisfies $e^{i 4 pi / 4} = -1$.
background
The module defines the eight-tick structure as the fundamental discrete clock with phases at multiples of pi/4. The phase definition computes the real value k pi /4 for each k in Fin 8. The phaseExp definition wraps this argument in the complex exponential exp(i times phase k). Upstream results include the phase definition itself and the phaseExp definition, which records that the eighth power of each phase yields one by periodicity.
proof idea
The proof unfolds phaseExp and phase to expose the argument 4 times pi over 4. It establishes that i times this argument equals i pi via push_cast followed by ring. Rewriting with the equality and invoking the library fact Complex.exp_pi_mul_I reduces the expression directly to negative one.
why it matters
This result supplies the fermion sign input to the spin_statistics_key theorem, which pairs it with the identity phase at zero. It feeds downstream theorems in SpinStatistics and QFT.SpinStatistics, including fermion_rotation_phase_neg_one and fermion_phase_from_foundation. In the framework it realizes the eight-tick octave step and supplies the phase sign required for the spin-statistics connection.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.