pith. machine review for the scientific record. sign in
def definition def or abbrev high

k_B

show as:
view Lean formalization →

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.

claimThe 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 in Recognition Science

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.

scope and limits

formal statement (Lean)

 110noncomputable def k_B : ℝ := 1.380649e-23

proof body

Definition body.

 111
 112/-- **THEOREM IC-002.8**: The Landauer energy k_B T ln(2) is positive for T > 0.
 113    This is the minimum energy cost to erase one bit of information. -/

used by (40)

From the project-wide theorem graph. These declarations reference this one in their body.

… and 10 more

depends on (21)

Lean names referenced from this declaration's body.