computation_has_nonzero_energy_cost
plain-language theorem explainer
The theorem establishes that the Landauer energy cost k_B T ln(2) is strictly positive for any positive temperature T. Physicists working on thermodynamic limits of computation would cite this result when bounding the minimum energy per bit erasure. The proof is a direct application of the positivity of the Landauer energy expression already established in the module.
Claim. For every real number $T > 0$, $k_B T$ ln$2 > 0$, where $k_B$ is the Boltzmann constant.
background
The module derives fundamental limits of computation in Recognition Science from temporal discreteness, irrational constants such as phi, and the Landauer erasure cost. The Boltzmann constant is defined as the noncomputable real 1.380649e-23 J/K. The upstream theorem landauer_energy_pos states: 'The Landauer energy k_B T ln(2) is positive for T > 0. This is the minimum energy cost to erase one bit of information.' A parallel result in InformationIsLedger gives the same positivity via the J-cost of 2-to-1 erasure.
proof idea
The proof is a one-line wrapper that applies the landauer_energy_pos theorem from the same module. That theorem unfolds the definition of k_B and invokes mul_pos twice followed by norm_num to obtain strict positivity.
why it matters
This declaration supplies IC-002.10 in the computation limits structure, confirming that the Landauer bound is nonzero and therefore no computation occurs for free in thermodynamic equilibrium. It supports the module's key results on thermodynamic floors and connects to the Recognition Science emphasis on positive J-cost for information erasure. The result closes the positivity step needed before discussing maximum rates and Bremermann limits.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.