k_B
plain-language theorem explainer
The declaration supplies the numerical value of the Boltzmann constant in SI units for thermodynamic calculations. Researchers deriving partition functions from ledger sums cite it when converting J-costs to physical energies and temperatures. It is introduced as a direct constant assignment matching the 2019 SI exact value.
Claim. The Boltzmann constant is defined by the assignment $k_B := 1.380649 × 10^{-23}$ (in J/K).
background
The PartitionFunction module derives the statistical mechanics partition function Z as a sum over ledger configurations weighted by J-cost, with Z = Σ exp(-β E_i) where β = 1/(k_B T). Temperature is the inverse of the Lagrange multiplier β. Upstream results include the definition of k_B in ComputationLimitsStructure as the anchor for the Landauer energy k_B T ln(2) and parallel definitions in the BekensteinHawking and PageCurve modules for Planck-scale relations.
proof idea
This is a one-line definition that directly assigns the SI value 1.380649e-23 to the real number k_B. No lemmas or tactics are applied.
why it matters
This constant supplies the physical scale that converts abstract ledger J-costs into laboratory temperatures. It feeds the theorem thermal_energy_at_unit_T relating thermal energy at unit T to ln(φ) and supports engineering certificates such as the room-temperature superconductivity structure. It realizes the link from the forcing chain's phi-ladder to observable thermodynamics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.