landauer_room_temp_value
plain-language theorem explainer
At room temperature $T=300\,\mathrm{K}$, the Landauer erasure energy $k_B T\ln 2$ is recorded as about $2.87\times 10^{-21}\,\mathrm{J}$. Anyone citing the INFO-004 Landauer-from-$\tau_0$ development would use this as the conventional SI anchor. The Lean statement is literally $\mathrm{True}$, discharged by `trivial`; the numerical claim lives only in the comment.
Claim. At temperature $T = 300\,\mathrm{K}$, the Landauer energy satisfies $k_B T \ln 2 \approx 2.87 \times 10^{-21}\,\mathrm{J}$, where $k_B = 1.380649 \times 10^{-23}\,\mathrm{J/K}$ is Boltzmann's constant.
background
Module INFO-004 aims to derive Landauer's bound from Recognition Science's fundamental recognition time $\tau_0$. Landauer's principle states that erasing one bit costs at least $E_{\min} = k_B T \ln 2$ in heat. The module frames erasure as recognize-then-forget, with a $J$-cost whose thermodynamic floor is that expression, and with $\tau_0$ setting the rate at which the cost is paid.
Locally, $k_B$ is fixed at the CODATA value $1.380649\times 10^{-23},\mathrm{J/K}$ (same constant appears in ComputationLimitsStructure, BekensteinHawking, and PartitionFunction). Sibling definitions supply room temperature ($300,\mathrm{K}$) and the Landauer energy $k_B T\ln 2$. The present declaration only pins the conventional SI magnitude of that product at $300,\mathrm{K}$.
proof idea
Term proof of True by trivial. No lemma about $k_B$, temperature, or $\ln 2$ is invoked. The approximate equality $k_B\times 300\times\ln 2\approx 2.87\times 10^{-21},\mathrm{J}$ is documentation only; Lean does not compute or certify the float.
why it matters
Gives the SI room-temperature anchor inside the INFO-004 Landauer-from-$\tau_0$ thread (patent/paper target: ultra-low-power computing near the Landauer limit; thermodynamics of information from RS). Sibling results (landauer_positive, landauer_from_tau0, jcost_equals_thermodynamic, minimumErasurePower) are where the actual RS content lives: positivity of $k_B T\ln 2$, the $\tau_0$ link, and equality of $J$-cost with the thermodynamic bound. Nothing downstream currently depends on this declaration (used_by empty). It does not touch T0–T8, RCL, or the $\phi$-ladder; it is a numerical checkpoint, not a forcing step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.