temperature_thermodynamic
plain-language theorem explainer
The declaration proves positivity of temperature for any System of energy levels whenever the inverse-temperature parameter beta exceeds zero. A researcher deriving the Boltzmann distribution from J-cost would cite it to confirm thermodynamic consistency in the RS setting. The proof is a one-line term reduction that unfolds the temperature definition and applies the reciprocal-positivity lemma.
Claim. Let $T(beta) := 1/beta$. For a System (a nonempty list of energy levels) and any real $beta > 0$, $T(beta) > 0$.
background
The BoltzmannDistribution module derives the Boltzmann form $P_i = exp(-beta E_i)/Z$ from Recognition Science's J-cost functional under a fixed total-cost constraint, with beta arising as the Lagrange multiplier. A System is a structure whose sole data is a nonempty list of EnergyLevel entries. Upstream, entropy is defined as total defect of a configuration (zero defect yields minimum entropy), and the module imports the J-cost primitives together with spectral and anchor constructions.
proof idea
The term proof unfolds the definition of temperature (reducing it to the reciprocal of beta) and applies the Mathlib lemma one_div_pos.mpr directly to the hypothesis beta > 0. The System argument is unused.
why it matters
The result supplies the sign of temperature required for the thermodynamic reading of the partition function and probabilities inside the RS derivation of statistical mechanics. It closes a basic consistency step in the module whose target is the paper proposition on Boltzmann statistics from J-cost, sitting downstream of the entropy-as-defect definition and upstream of normalized probability constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.