fermi_dirac_bounded
plain-language theorem explainer
The Fermi-Dirac occupation probability lies strictly between zero and one for any real energy and chemical potential when temperature is positive. A physicist extracting quantum statistics from ledger constraints would cite this to confirm consistency with Pauli exclusion. The proof is a direct algebraic verification that unfolds the explicit formula and applies positivity of the exponential together with linear arithmetic.
Claim. For all real numbers $E, mu, T$ with $T > 0$, the Fermi-Dirac distribution satisfies $0 < 1/ (exp((E - mu)/T) + 1) < 1$.
background
The Thermodynamics.FermiDirac module derives the Fermi-Dirac distribution from the odd-phase ledger constraint in Recognition Science's eight-tick structure. Fermions carry odd 8-tick phase, enforcing antisymmetry so that each state holds at most one particle. The explicit definition is the standard form $f(E, mu, T) = 1 / (exp((E - mu)/T) + 1)$, where the added 1 encodes the exclusion rule. The local setting is maximum-entropy counting under fixed average energy and particle number, as stated in the module documentation on quantum statistics from ledger structure.
proof idea
The tactic proof unfolds the fermiDirac definition to obtain the explicit rational expression. It splits the conjunction goal. The strict lower bound is obtained by applying one_div_pos.mpr after invoking positivity of the exponential. The strict upper bound rewrites the target inequality as exp((E-mu)/T) + 1 > exp((E-mu)/T), which follows from positivity, then closes both sides with linarith.
why it matters
This theorem supplies the elementary bound required for any ledger-derived Fermi-Dirac form to be physically admissible. It directly supports the THERMO-009 derivation of quantum statistics from the odd-phase ledger inside the eight-tick octave. The result closes a basic consistency check before further thermodynamic constructions that rely on the same distribution.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.