fermion_phase_from_foundation
plain-language theorem explainer
The declaration establishes that the phase factor after four steps of the eight-tick cycle equals exactly -1. This supplies the minus sign required for fermionic antisymmetry in the Recognition Science derivation of spin-statistics. Researchers working on discrete-time foundations of quantum field theory would cite the result. The proof is a one-line wrapper that invokes the pre-proven phase_4_is_minus_one lemma from the Foundation.EightTick module.
Claim. The complex phase factor after four ticks in the eight-tick cycle satisfies $e^{i 4 pi / 4} = -1$, where the phase at tick index $k$ is defined by $k pi / 4$ and the exponential map is $exp(i times phase(k))$.
background
In Recognition Science the eight-tick cycle is the fundamental evolution period, with each tick advancing phase by $pi/4$. The function phase maps an index $k$ in Fin 8 to $k pi /4$, while phaseExp returns the complex value $exp(i times phase(k))$. The upstream lemma phase_4_is_minus_one proves that this exponential equals -1 at $k=4$, which corresponds to a half-turn and produces the fermion sign. The local setting is the QFT-001 module whose documentation states that half-integer spin particles require two full cycles for identity while integer-spin particles require one, with the phase mechanism directly yielding $exp(pi i n) = -1$ for odd $n$.
proof idea
The proof is a one-line wrapper that applies the lemma phase_4_is_minus_one from Foundation.EightTick. That lemma unfolds phaseExp and phase, reduces the argument to $i pi$, and invokes the identity $exp(i pi) = -1$.
why it matters
This theorem supplies the fermionic minus sign that is conjoined with the bosonic +1 and the vacuum sum in the parent result spin_statistics_from_foundation. It realizes the T7 eight-tick octave landmark by showing how the discrete cycle produces the observed Fermi-Dirac sign after a $2 pi$ rotation. The result closes one explicit link from the forcing-chain foundation to the spin-statistics connection described in the module documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.