exchange_sign_fermion
plain-language theorem explainer
exchange_sign_fermion fixes the fermionic exchange sign at -1 by equating it to the phase under 2π rotation of the relative coordinate. Researchers deriving spin-statistics from the eight-tick ledger in Recognition Science cite this to link the 4-tick period to antisymmetry. The proof is a direct one-line reference to the explicit computation for period 4.
Claim. For a fermionic state with 4-tick period, the phase accumulated under a single $2π$ rotation of the relative coordinate equals $-1$, which sets the exchange sign under two-particle interchange.
background
The SpinStatistics module derives the full spin-statistics connection from the eight-tick ledger. rotationPhase(period) is defined as phaseExp of (4 mod 8) and computes the complex phase acquired under 2π rotation. The upstream theorem fermion_rotation_phase_neg_one states that this phase equals -1 precisely when the period is 4, corresponding to spin-1/2 states that anticommute under exchange.
proof idea
This is a one-line wrapper that applies fermion_rotation_phase_neg_one, which unfolds the definition of rotationPhase and invokes the explicit evaluation phase_4_is_minus_one.
why it matters
The result supplies the fermionic case required by spin_statistics_theorem, which equates the exchange sign of a two-particle state to the rotation phase under 2π. It realizes the eight-tick octave distinction (4-tick versus 8-tick periods) that forces antisymmetric versus symmetric statistics, as described in the module doc and the paper RS_Spin_Statistics_Theorem.tex.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.