fermi_from_odd_phase
plain-language theorem explainer
The declaration establishes that the complex exponential of the phase at the fourth position in the 8-tick cycle equals negative one, supplying the antisymmetric sign for fermions that produces the plus-one term in the Fermi-Dirac occupation factor. Researchers connecting the Recognition Science eight-tick structure to spin-statistics and thermodynamic distributions would cite it when tracing Pauli exclusion to the phase assignment. The proof is a one-line term wrapper that pairs the upstream phase lemma with a trivial second conjunct.
Claim. $e^{i phi_4} = -1$ where $phi_4 = pi$, which encodes the fermion exchange sign and enforces the occupation factor $f(E) = [exp((E - mu)/T) + 1]^{-1}$.
background
The J-Cost to Thermodynamics Bridge module links the J-cost functional J(x) = (x + x^{-1})/2 - 1 to thermodynamic distributions by treating temperature as the Lagrange multiplier for average J-cost constraints. The eight-tick phases are defined as k pi /4 for k in Fin 8, with phaseExp computing the complex exponential exp(i * phase k). Upstream results include the definition of tick as the fundamental RS time quantum and the theorem phase_4_is_minus_one whose doc-comment states: 'Phase at k=4 gives -1 (fermion phase). This is the key to antisymmetry under particle exchange.'
proof idea
The proof is a one-line term wrapper that applies the upstream lemma phase_4_is_minus_one to obtain the first conjunct and pairs it with trivial for the second conjunct.
why it matters
This theorem supplies the phase sign that feeds the FermiDirac module's fermi_from_odd_phase result, which states fermions have half-integer spin giving odd 8-tick phase leading to antisymmetry and Pauli exclusion. It fills the module's listed step from odd-phase constraint to the +1 in the Fermi-Dirac denominator and connects directly to the eight-tick octave landmark. It touches the open question of completing the full J-cost derivation of the distribution without extra hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.