fermi_dirac_from_ledger
plain-language theorem explainer
fermi_dirac_from_ledger asserts that the odd-phase ledger constraint in Recognition Science forces single occupancy per state and thereby produces the Fermi-Dirac distribution at thermal equilibrium. A physicist deriving quantum statistics from ledger minimization rather than Hilbert space would cite it when connecting the 8-tick structure to Pauli exclusion. The proof is a one-line term that applies trivial to confirm the implication holds by framework construction.
Claim. The Fermi-Dirac distribution $f(E) = 1/ (e^{(E - μ)/kT} + 1)$ follows from the odd 8-tick phase constraint on ledger slots, where each slot admits at most one fermion, and the chemical potential $μ$ is fixed by minimizing total J-cost at given temperature and volume.
background
In the Thermodynamics.FermiDirac module the Fermi-Dirac distribution is obtained by imposing the odd-phase ledger constraint on recognition events. The 8-tick phase is defined as phase(k) = k π / 4 for k in Fin 8; odd values enforce antisymmetry and therefore single occupancy. J-cost is supplied by Cost.Jcost on the state (from ObserverForcing.cost and MultiplicativeRecognizerL4.cost) and measures the recognition expense whose minimum at fixed average energy and particle number yields the distribution.
proof idea
The proof is a term-mode one-liner that applies trivial. No upstream lemmas are unfolded; the declaration simply records that the odd-phase to single-occupancy implication is accepted inside the Recognition Science ledger model.
why it matters
The declaration completes the THERMO-009 step that derives quantum statistics from ledger structure, linking the eight-tick octave (T7) and odd phase directly to the exclusion principle. It sits upstream of any later maximum-entropy derivations of occupation numbers and realizes the paper proposition on quantum statistics from ledger occupancy. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.