landauer_energy_pos
plain-language theorem explainer
The theorem establishes that Boltzmann's constant times any positive temperature times the natural log of 2 is strictly positive. Researchers deriving thermodynamic bounds on computation cite it to enforce a nonzero energy floor for bit erasure. The proof unfolds the numerical definition of k_B then chains the mul_pos lemma with norm_num and Real.log_pos to confirm each factor is positive.
Claim. For every real number $T > 0$, $k_B T$ ln$2 > 0$, where $k_B$ is Boltzmann's constant.
background
The IC-002 module derives computation limits from temporal discreteness (the fundamental tick as minimum time quantum), irrationality of phi, and the Landauer erasure cost. The Landauer energy is defined as the minimum cost to erase one bit of information, expressed as $k_B T$ ln$2$. The constant $k_B$ is introduced as the numerical value 1.380649e-23 J/K. This result rests on the upstream positivity theorem in InformationIsLedger, which states that for any $T > 0$ the product $k_B$ ln$2$ times $T$ is positive and interprets the cost via the J-function applied to a 2-to-1 state reduction.
proof idea
The term-mode proof first unfolds the definition of k_B. It then applies mul_pos twice to split the three-factor product into separate positivity claims. norm_num dispatches the constant positivity of k_B and of ln 2, exact hT supplies the temperature hypothesis, and Real.log_pos confirms ln 2 > 0.
why it matters
The declaration supplies the core positivity fact required by the downstream theorem computation_has_nonzero_energy_cost, which universalizes the bound to assert that no computation occurs for free at positive temperature. It occupies the IC-002.8 slot inside the ic002_certificate and directly implements the Landauer component of the module's four-source limit structure. The result anchors the thermodynamic floor within Recognition Science's derivation of limits from the recognition composition law and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.