landauer_scales_with_temp
plain-language theorem explainer
The theorem establishes that the Landauer energy cost k_B T ln 2 increases strictly with temperature for any T2 > T1 > 0. Researchers deriving thermodynamic floors on bit erasure in physical computers would cite this when bounding energy requirements at different operating temperatures. The short tactic proof unfolds the numerical definition of k_B, records positivity of ln 2 and the constant via norm_num, and closes the inequality with nlinarith.
Claim. For all real numbers $T_1 > 0$ and $T_2 > 0$ satisfying $T_2 > T_1$, the inequality $k_B T_2$ ln$2 > k_B T_1$ ln$2$ holds, where $k_B$ is the Boltzmann constant.
background
Module IC-002 derives fundamental computation limits from Recognition Science. The three sources are temporal discreteness (tick as minimum time quantum), irrationality of phi (preventing exact finite simulation), and the Landauer erasure cost k_B T ln 2 that sets the thermodynamic floor. The sibling definition k_B supplies the numerical value 1.380649e-23 in SI units and is accompanied by the positivity statement IC-002.8. Upstream results include the structural definitions of empirical programs and simplicial ledgers that supply the ledger context in which erasure costs are evaluated.
proof idea
The tactic proof first unfolds the definition of k_B to expose its numerical value. It then records the auxiliary facts that ln 2 is positive (via Real.log_pos with norm_num) and that the constant 1.380649e-23 is positive (via norm_num). The final nlinarith step combines these facts with the hypothesis T2 > T1 to obtain the strict inequality.
why it matters
The result occupies the IC-002.9 position inside the computation-limits structure and is referenced by the IC-002 status certificate. It directly instantiates the framework claim that Landauer erasure supplies a positive, temperature-dependent energy floor, consistent with the Recognition Science derivation of physical constants from the forcing chain (T0-T8) and the Recognition Composition Law. No open scaffolding questions are addressed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.