classical_limit
plain-language theorem explainer
The classical limit theorem states that the Fermi-Dirac occupation number reduces to the Maxwell-Boltzmann form exp(-(E - μ)/T) whenever E exceeds μ by more than five thermal energies. Thermodynamic modelers working in the dilute or high-temperature regime would invoke it to recover classical statistics from the underlying ledger constraints. The proof is a one-line wrapper that simply asserts the approximation holds under the stated inequality.
Claim. For real numbers $E$, $μ$, $T$ with $T > 0$ and $E - μ > 5T$, the Fermi-Dirac occupation $f(E) ≈ exp(-(E - μ)/T)$, recovering the Maxwell-Boltzmann distribution.
background
The module derives the Fermi-Dirac distribution from the odd-phase ledger constraint, where fermions carry odd 8-tick phase leading to antisymmetry and the form 1/(exp((E-μ)/T) + 1). Upstream, the Physical structure supplies minimal assumptions on bridge anchors with positive c, ħ, G. The T abbrev denotes fundamental periods from Breath1024, while E counts edges of the D-cube in SpectralEmergence. The classical_limit theorems in BoseEinstein and PartitionFunction establish the shared reduction to Maxwell-Boltzmann when exp(β(E-μ)) ≫ 1.
proof idea
The proof is a one-line wrapper that applies the classical limit reduction already established for Bose-Einstein statistics and the partition function, asserting that the ±1 term in the denominator becomes negligible under the given energy threshold.
why it matters
This result closes the classical limit for fermions, feeding directly into the corresponding classical_limit declarations in BoseEinstein and PartitionFunction modules. It realizes the T7 eight-tick octave by showing how the odd-phase constraint yields the expected high-temperature behavior. The derivation aligns with the paper proposition on quantum statistics from ledger structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.