halfCyclePhase
plain-language theorem explainer
halfCyclePhase assigns the complex phase exp(π i s.value) to each spin s, capturing the factor after a π rotation equivalent to half an 8-tick cycle. Researchers deriving the spin-statistics theorem from discrete time structures cite this when linking 8-tick periodicity to the sign change under particle exchange for half-integer spins. The definition is a direct one-line wrapper around Complex.exp applied to π times the imaginary unit times the spin value.
Claim. For a spin quantum number $s$, the half-cycle phase is $e^{i π s}$.
background
The QFT-001 module derives the spin-statistics theorem from Recognition Science's 8-tick cycle, where a 2π rotation traverses the full cycle and half-integer spins require two cycles for identity. The Spin structure encodes the quantum number via an integer field twice (twice the spin value) with a nonnegativity constraint. Upstream, the phase definition in EightTick supplies the discrete angles kπ/4 for k = 0 to 7, establishing the underlying periodicity that this half-cycle phase samples at the 4-tick mark.
proof idea
The definition is a one-line wrapper that multiplies the spin value by π and the imaginary unit, then applies Complex.exp.
why it matters
This definition supplies the explicit phase factor for the 8-tick derivation of spin-statistics in the Recognition framework. It implements the phase mechanism step in the module target, where the eight-tick octave (T7) produces +1 for integer spins and -1 for half-integer spins under exchange. It connects directly to the phase accumulation rule that distinguishes fermions from bosons.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.