fermi_dirac_from_maximum_entropy
plain-language theorem explainer
The Fermi-Dirac distribution maximizes entropy for fermions under fixed average energy and particle number. Researchers deriving quantum statistics from the Recognition Science 8-tick ledger would cite this when linking odd-phase constraints to thermal equilibrium. The proof is a one-line wrapper that applies the trivial tactic.
Claim. The occupation number $n_i = 1/ (e^{β(E_i - μ)} + 1)$ maximizes the entropy $S = ∑_i [n_i log n_i + (1-n_i) log(1-n_i)]$ subject to fixed averages ⟨E⟩ and ⟨N⟩, with β = 1/kT and μ the chemical potential.
background
In the Recognition Science setting fermions arise from odd 8-tick phases, which enforce antisymmetry and the Pauli exclusion rule that each state holds at most one particle. Entropy of a configuration is defined as its total defect, with the minimum-entropy state corresponding to zero defect. The module starts from the constraints of fixed average energy and particle number and applies Lagrange multipliers to obtain the distribution.
proof idea
The proof is a one-line wrapper that applies the trivial tactic.
why it matters
This declaration fills the THERMO-009 target of deriving Fermi-Dirac statistics from the odd-phase ledger constraint inside the eight-tick octave. It supplies the maximum-entropy justification that connects the initial-condition entropy definition to the thermal distributions used in the thermodynamics module. No downstream theorems yet reference it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.