landauer_constant_pos
plain-language theorem explainer
Recognition Science proves the Landauer constant k_B ln(2) is strictly positive, supplying the minimal energy cost for erasing one bit. Information theorists and physicists working on thermodynamic bounds in discrete frameworks cite this as the RS embedding of Landauer's principle. The proof is a direct term reduction that unfolds the constant and applies multiplication positivity together with the known sign of the natural logarithm at 2.
Claim. Boltzmann's constant times the natural logarithm of 2 is strictly positive: $k_B$ ln$2 > 0$.
background
The InformationIsLedger module identifies every recognition event with a ratio x > 0 whose J-cost J(x) = (x + x^{-1})/2 - 1 measures information content. The module lists eight core theorems, the last of which is the Landauer principle that bit erasure dissipates at least k_B T ln(2) energy. Upstream results supply the real-number ordering, the definition of the fundamental period T, and the unit elements in the logic integers and rationals used to construct the constant.
proof idea
The term-mode proof unfolds the definition of k_B_ln2 and applies the mul_pos lemma. Norm_num discharges the positivity of k_B while Real.log_pos, after a norm_num argument confirming the argument exceeds 1, discharges the positivity of ln(2).
why it matters
This theorem supplies the final positivity step inside the IC-001 certificate that information is the ledger. It is invoked directly by the companion result landauer_energy_pos, which lifts the constant to E_min(T) = k_B T ln(2) > 0 for any T > 0. The placement confirms that information erasure carries positive J-cost, consistent with the symmetry J(x) = J(1/x) and the infinite cost of the nothingness limit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.