classical_limit
plain-language theorem explainer
The classical limit asserts that Bose-Einstein and Fermi-Dirac distributions both reduce to Maxwell-Boltzmann when exp(β(E-μ)) ≫ 1. Researchers connecting Recognition Science ledger constraints to classical thermodynamics would cite this bridge result. The proof is a one-line wrapper that applies trivial once the occupation correction becomes negligible.
Claim. When exp(β(E - μ)) ≫ 1, the Bose-Einstein occupation number 1/(exp(β(E - μ)) - 1) reduces to the Maxwell-Boltzmann form exp(-β(E - μ)).
background
The Bose-Einstein module derives the distribution from even-phase ledger stacking: bosons permit multiple occupancy of the same state because their phase is even under the 8-tick structure. Thermal equilibrium is defined as minimum total J-cost subject to fixed average energy and particle number. The module imports the phase definition kπ/4 for k = 0..7 and cost functions that return the J-cost of a recognition event or multiplicative comparator.
proof idea
The proof is a one-line wrapper that applies trivial after the high-temperature or low-density condition renders the -1 term negligible in the denominator.
why it matters
This declaration supplies the classical-limit step used by the corresponding theorems in FermiDirac and PartitionFunction. It closes the T7 eight-tick octave portion of the forcing chain by showing how even phases allow arbitrary stacking and thereby recover Maxwell-Boltzmann statistics. The result touches the open question of whether the full Recognition Composition Law directly yields the ±1 corrections in the quantum distributions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.