k_B
plain-language theorem explainer
The declaration supplies the SI numerical value of the Boltzmann constant as 1.380649 × 10^{-23} J/K. Physicists and engineers anchoring Recognition Science computation limits to laboratory temperatures cite it when converting between RS-native energy scales and measurable thermal energies. The definition consists of a direct numerical assignment with no reduction steps or lemmas.
Claim. The Boltzmann constant is defined by $k_B := 1.380649 × 10^{-23}$ J/K.
background
The module IC-002 derives fundamental limits of computation from Recognition Science. These limits arise from temporal discreteness (the tick τ₀ as minimum time quantum), irrationality of φ (preventing exact finite rational simulation), and the Landauer erasure cost: erasing one bit requires energy k_B T ln(2). This sets a thermodynamic floor on computation, alongside the Bremermann limit E × t ≥ ħ/2.
proof idea
Direct definition assigning the numerical value 1.380649e-23 to k_B. No lemmas are applied and no tactics are used.
why it matters
This definition anchors the Landauer bound within the RS framework and feeds into downstream results such as thermal_energy_at_unit_T (which relates the RS-native k_R to ln(φ)) and engineering certificates for room-temperature superconductivity (which compare k_B T_room to the coherence quantum E_coh = φ^{-5}). It supplies the external SI anchor required by the module's computation-limits structure, connecting RS-native units (c=1, ħ=φ^{-5}) to CODATA values.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.