k_B_ln2
plain-language theorem explainer
The definition supplies the numerical value of the Landauer constant k_B ln(2) in joules per kelvin using the CODATA Boltzmann constant. Information theorists and physicists working on thermodynamic limits of computation cite it when establishing minimum energy costs for bit erasure inside the Recognition Science ledger. It is introduced as a direct real-number assignment with no lemmas or reductions.
Claim. The Landauer constant is defined by $k_B = 1.380649 × 10^{-23}$ J/K and equals $k_B ln 2$ (in J/K).
background
The module InformationIsLedger asserts that information is the physical ledger: every recognition ratio x > 0 carries a J-cost J(x) ≥ 0, with J(x) = 0 only at x = 1. J-cost is introduced via PhiForcingDerived.of as the structure of (ℝ₊, ×) and the calibration of J. The module lists eight core theorems, the last of which is the Landauer principle: erasing information costs at least k_B T ln(2). Upstream results include LedgerFactorization.of for the underlying group structure and PhiForcingDerived.of for the explicit J-cost definition.
proof idea
This declaration is a direct definition that multiplies the empirical value 1.380649e-23 by Real.log 2. No lemmas are invoked; the assignment is used verbatim by the two downstream positivity theorems in the same module.
why it matters
The constant realizes module claim 8 and feeds landauer_constant_pos and landauer_energy_pos, which prove k_B ln(2) > 0 and k_B T ln(2) > 0 for T > 0. It supplies the thermodynamic scale that converts the abstract J-cost of a 2-to-1 erasure (J(2) = 1/4) into physical energy, linking the Recognition Composition Law and the eight-tick octave to observable dissipation. No open scaffolding remains at this node.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.