fermion_rotation_phase_neg_one
plain-language theorem explainer
The theorem asserts that the rotation phase for a 4-tick fermion equals -1. Quantum theorists deriving spin-statistics relations from discrete time structures would cite this result. The proof is a one-line wrapper that unfolds the rotationPhase definition and invokes the exact phase evaluation at tick 4.
Claim. The phase factor acquired by a fermion under a full $2π$ rotation equals $-1$.
background
The SpinStatistics module derives the spin-statistics theorem from the RS eight-tick ledger. Phases are defined as $kπ/4$ for $k$ in Fin 8, with the complex exponential phaseExp(k) = exp(i · phase(k)). The rotationPhase function for fermions selects the 4-tick case, which corresponds to the half-octave point. Upstream result phase_4_is_minus_one states: 'Phase at k=4 gives -1 (fermion phase). This is the key to antisymmetry under particle exchange.' The module documentation notes that this forces antisymmetry for spin-1/2 states under 2π rotation.
proof idea
This is a one-line wrapper proof. It unfolds the definition of rotationPhase and applies the exact theorem phase_4_is_minus_one from the EightTick module, which reduces the phase via the identity exp(iπ) = -1.
why it matters
The result supplies the fermion rotation phase directly to exchange_sign_fermion (which derives the exchange sign -1), to pauli_exclusion (which obtains the exclusion principle via ψ = -ψ implying ψ = 0), and to spin_statistics_certificate (which certifies the full theorem). It realizes the eight-tick octave (T7) for the fermion half of the spin-statistics connection, as referenced in RS_Spin_Statistics_Theorem.tex. The certificate confirms no hypotheses remain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.