maxwellBoltzmann
plain-language theorem explainer
The declaration supplies the Maxwell-Boltzmann distribution as the classical limit of the Fermi-Dirac and Bose-Einstein forms inside the Recognition Science ledger framework. Workers on thermodynamic reductions from the 8-tick odd-phase constraint cite it when high temperature or low density makes the exponential dominate. The definition is a direct one-line application of the real exponential to the reduced energy.
Claim. The Maxwell-Boltzmann distribution is $f(E,μ,T)=exp(-(E-μ)/T)$, where $E$ denotes single-particle energy, $μ$ the chemical potential, and $T$ the temperature (with $k_B=1$).
background
The module derives Fermi-Dirac statistics from the odd-phase ledger constraint of the 8-tick structure: fermions occupy states with phase factor -1, Pauli exclusion enforces 0-or-1 occupancy, and minimum J-cost at fixed total energy and particle number yields the distribution. The supplied definition records the classical reduction stated in the module comment: both Fermi-Dirac and Bose-Einstein collapse to this exponential when exp((E-μ)/T)≫1. Upstream results supply the period T (Breath1024), the D-cube edge count E (SpectralEmergence), and triangular numbers (Gap45.SyncMinimization) that underpin the spectral and minimization scaffolding used throughout the thermodynamics layer.
proof idea
The definition is a direct one-line wrapper that applies Real.exp to the negated reduced energy (E-μ) divided by T.
why it matters
This definition completes the classical-limit case required by the THERMO-009 derivation of quantum statistics from ledger structure. It supplies the high-T or low-density bridge between the Fermi-Dirac and Bose-Einstein forms and the Maxwell-Boltzmann exponential, consistent with the Recognition Science reduction to minimum J-cost and the eight-tick octave. The placement supports the paper proposition on quantum statistics from ledger structure and closes the classical endpoint of the odd-phase constraint.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.