fermi_bounded
plain-language theorem explainer
The Fermi-Dirac occupation number lies strictly above zero and at most one for any positive temperature. Thermodynamic calculations in the Recognition framework cite this bound to keep derived probabilities admissible. The proof unfolds the explicit formula then applies positivity of the exponential together with linarith on the resulting inequalities.
Claim. For all real numbers $E$, $μ$, $T$ with $T > 0$, the Fermi-Dirac distribution satisfies $0 < 1/ (exp((E - μ)/T) + 1) ≤ 1$.
background
The JCostThermoBridge module links Recognition Science J-cost minimization to thermodynamic distributions. The Fermi-Dirac form arises from the odd-phase constraint on the eight-tick cycle, while the Boltzmann factor emerges directly as the J-cost minimizer. Upstream, the phase definition from EightTick supplies the periodic angles $kπ/4$ that enforce the sign difference between Fermi and Bose cases, and SpectralEmergence.E supplies the edge counting that fixes spatial dimension three.
proof idea
Unfold the definition of fermiDirac. Split the conjunction with constructor. For the lower bound apply one_div_pos.mpr after Real.exp_pos shows the exponential term is positive. For the upper bound establish that the denominator is at least one and positive, rewrite via div_le_one, then finish with linarith.
why it matters
The bound confirms that occupation numbers obtained from RS phase constraints remain valid probabilities between zero and one. It supports the module's derivation of fermi_from_odd_phase_jcost by supplying the elementary range property required for thermodynamic consistency. In the larger chain it closes the passage from eight-tick phases through spin-statistics to the physical distributions used for the alpha band and mass ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.