standardBoltzmann
plain-language theorem explainer
This definition supplies the classical Boltzmann factor exp(-E/T) as the reference weight against which J-cost derived distributions are compared in the thermodynamics bridge. Physicists working on emergent statistics from recognition costs would reference it when contrasting standard thermal ensembles with those minimizing average J-cost. The definition is a direct one-line abbreviation of the exponential function applied to the negative energy-temperature ratio.
Claim. The standard Boltzmann weight for energy $E$ at positive temperature $T$ is defined as $e^{-E/T}$.
background
The module establishes the formal link between Recognition Science J-cost and thermodynamic distributions. J-cost arises as the derived cost of a multiplicative recognizer comparator and as the cost of any recognition event. Upstream results include the fundamental period T from Breath1024 and the edge count E of the D-cube from SpectralEmergence, which together set the discrete structure underlying continuous thermal limits. Temperature enters as the Lagrange multiplier enforcing the J-cost constraint rather than an independent parameter.
proof idea
This is a one-line definition that directly applies the real exponential function to the negative ratio of energy to temperature.
why it matters
This definition anchors the comparison baseline for the J-cost Boltzmann weights and related results in the module. It supports the main theorems on energy proportional to J-cost and on Boltzmann weights minimizing expected J-cost. It connects to the framework's T5 J-uniqueness and the reduction of thermal statistics from 8-tick phases and ledger balance.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.