fermi_from_odd_phase
plain-language theorem explainer
Odd 8-tick phase for fermions enforces antisymmetry under particle exchange, which imposes Pauli exclusion and produces the Fermi-Dirac occupation number after entropy maximization under fixed average energy and particle number. Researchers deriving quantum statistics from ledger constraints would cite this link. The argument reduces directly to the trivial proposition once the phase sign at k=4 is fixed from the eight-tick definition.
Claim. Fermions carry half-integer spin and therefore an odd phase in the eight-tick cycle, satisfying $e^{iπ}=-1$. This forces antisymmetric wave functions, single occupancy per state, and, upon maximizing entropy subject to fixed average energy and particle number, the occupation number $f(E)=1/ (e^{(E-μ)/kT}+1)$.
background
The eight-tick phase is the map sending each integer k in 0..7 to kπ/4. The value at k=4 equals π and therefore yields the exchange sign -1. In the local setting the module starts from the odd-phase ledger constraint: fermions obey this sign change, which prohibits double occupancy, and thermal equilibrium is defined as the minimum-J-cost state consistent with that constraint. Upstream, the phase definition supplies the explicit value at k=4 while the action and spectral-edge constructions supply the energy ledger that enters the constraints.
proof idea
The proof is a one-line wrapper that applies the trivial tactic. The accompanying comment records the entropy-maximization steps (Lagrange multipliers β=1/kT and α=-μ/kT applied to the binary-occupancy entropy) but the formal Lean reduction accepts the phase sign and antisymmetry implication without further expansion.
why it matters
The declaration supplies the direct bridge from the eight-tick phase structure to the Fermi-Dirac denominator in the thermodynamics module. It feeds the downstream result in JCostThermoBridge that isolates the +1 term from the k=4 phase value. The module presents the step as the core of the derivation of quantum statistics from ledger structure, closing the passage from T7 (eight-tick octave) through spectral emergence to observable thermal distributions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.