landauer_energy_pos
plain-language theorem explainer
Landauer's principle is realized as a theorem in Recognition Science: the minimum energy cost to erase one bit equals k_B T ln(2) and is strictly positive for every T > 0. Researchers deriving thermodynamic bounds on computation or reversible information processing cite this result when establishing that no erasure occurs at zero energy. The proof is a direct one-line term application of the mul_pos lemma to the already-established positivity of the Landauer constant and the hypothesis T > 0.
Claim. For every real number $T > 0$, the product $k_B T$ times the natural logarithm of 2 is strictly positive, where $k_B$ denotes Boltzmann's constant. This bound is the minimum energy required to erase one bit of information.
background
The module InformationIsLedger identifies every physical fact with a recognition event whose information content is the J-cost J(x) of the associated ratio x > 0. J(x) is defined by the formula (x + x^{-1})/2 - 1, vanishes only at x = 1, and is symmetric under x to 1/x. Upstream lemmas supply the cost function on recognition events (ObserverForcing.cost) and the derived cost on positive ratios (MultiplicativeRecognizerL4.cost), both of which reduce to this J-cost. The module lists the Landauer bound as core theorem 8, linking bit erasure (the 2-to-1 transition with J(2) = 1/4) to the temperature-dependent energy scale.
proof idea
The proof is a one-line term-mode wrapper that applies the mul_pos lemma directly to the positivity of the Landauer constant k_B ln 2 and the hypothesis that T > 0.
why it matters
The declaration completes the IC-001 series by supplying the thermodynamic cost of information erasure and feeds the IC-002 results on computation limits, including computation_has_nonzero_energy_cost (which asserts that no computation occurs for free) and the IC-002 status certificate. Within the Recognition Science framework it converts the positivity of J-cost for the bit-erasure ratio into the classical Landauer bound, realizing the eight-tick octave and phi-ladder scaling at the information-thermodynamic interface. No open scaffolding remains for this specific statement.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.