fermi_at_mu
plain-language theorem explainer
The declaration shows that the Fermi-Dirac occupation number equals one half exactly when energy equals the chemical potential. Researchers deriving quantum statistics from Recognition Science ledger constraints would cite this midpoint property. The proof is a direct term-mode reduction that unfolds the distribution definition and simplifies the resulting algebraic identity.
Claim. For the Fermi-Dirac distribution $f(E) = 1/ (e^{(E - μ)/T} + 1)$, the equality $f(μ) = 1/2$ holds for any real chemical potential $μ$ and temperature $T$.
background
The module derives the Fermi-Dirac distribution from Recognition Science's 8-tick structure under the odd-phase ledger constraint for fermions. The function fermiDirac(E, μ, T) is defined as 1 / (exp((E - μ)/T) + 1), with the +1 arising from Pauli exclusion via odd-phase antisymmetry. Upstream results include the equivalent definition in JCostThermoBridge that explicitly links the form to minimum J-cost at temperature T, the localRule step in CellularAutomata for successor tapes, and the period T from Breath1024.
proof idea
The term proof unfolds the fermiDirac definition, applies simp with the rule Real.exp_zero to replace the zero-argument exponential by 1, and closes with ring to confirm the identity equals 1/2.
why it matters
This anchors the Fermi-Dirac distribution at its half-occupancy point, consistent with the odd-phase ledger inside the eight-tick octave. It supplies the midpoint case in the derivation of quantum statistics from ledger structure described in the module documentation. No downstream theorems yet reference it, leaving open its role in broader thermodynamic chains such as zero-temperature limits or maximum-entropy derivations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.