kB_SI
plain-language theorem explainer
The Boltzmann constant supplies the exact SI value 1.380649 × 10^{-23} J/K as an external calibration anchor. Thermodynamic modules cite it when mapping RS-native J-costs to physical temperatures in kelvin. It enters through direct numerical assignment with no reduction steps or lemma invocations.
Claim. The Boltzmann constant equals $1.380649 × 10^{-23}$ J K$^{-1}$ (exact SI 2019 value).
background
The ExternalAnchors module isolates all empirical calibration data from the pure cost derivation. Module documentation states that the cost-first core must not import this module, preserving separation between quantities derived from the Recognition Composition Law and measured constants. The upstream constant scalar field definition supplies a mechanism for embedding fixed real values into field contexts used in related constructions.
proof idea
This is a direct definition that assigns the literal real number 1.380649e-23. No lemmas are applied and no tactics are used; the body consists solely of the numerical literal.
why it matters
It anchors the temperature scale for downstream thermodynamic constructions including Bose-Einstein condensation temperature and classical heat capacity. These appear in the ChemicalPotential and HeatCapacity modules. The anchor enables comparison of J-cost gradients with laboratory data while leaving the RCL core and phi-ladder derivations untouched.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.