fermiMuLowT
plain-language theorem explainer
The declaration encodes the standard low-T Sommerfeld expansion for Fermi-gas chemical potential as μ(T) ≈ E_F [1 - (π²/12)(kT/E_F)²]. Condensed-matter physicists and Recognition Science modelers cite it when treating Fermi-Dirac statistics below the degeneracy temperature. It is realized as a direct one-line algebraic expression that substitutes the SI Boltzmann constant.
Claim. The low-temperature chemical potential of an ideal Fermi gas is given by $μ(T) ≈ E_F (1 - (π²/12)(k_B T / E_F)²)$, where $E_F$ is the Fermi energy and $k_B$ is Boltzmann's constant.
background
In Recognition Science, chemical potential is the J-cost gradient with respect to particle number: particles flow to minimize total J-cost, and μ determines ledger occupation. The module THERMO-007 states μ = (∂F/∂N)_{T,V} and ties this quantity to the phi-ladder and Recognition Composition Law. The definition imports the exact SI anchor kB_SI = 1.380649 × 10^{-23} J/K together with structures for J-cost (PhiForcingDerived) and ledger factorization (DAlembert).
proof idea
Direct definition that substitutes the standard low-T expansion into the supplied expression. It applies the external constant kB_SI and performs the algebraic reduction without invoking additional lemmas or tactics.
why it matters
This definition supplies the Fermi-gas case required by the chemical-potential derivations in Thermodynamics.ChemicalPotential. It supports the claim that μ arises as a J-cost gradient and connects to the eight-tick octave and D = 3 spatial structure through ledger occupation. It leaves open the precise mapping of RS-native units onto measured Fermi energies in real materials.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.