landauerRoomTemp
plain-language theorem explainer
Landauer energy at room temperature (300 K) is the classical minimum cost of erasing one bit: E = k_B T ln 2. Thermodynamics-of-computation and efficiency-gap arguments cite this constant as the denominator against practical bit-erasure energy. The declaration is a one-line specialization of the temperature-dependent Landauer energy at T = 300.
Claim. Define the room-temperature Landauer energy by $E_{\mathrm{L}}(300\,\mathrm{K}) := k_B \cdot 300 \cdot \ln 2$, where $k_B$ is Boltzmann's constant and $T = 300$ is room temperature in kelvin.
background
Module INFO-004 targets the Landauer bound (minimum energy to erase one bit) from Recognition Science's fundamental timescale τ₀. Classically, Landauer's principle states that irreversible erasure of one bit dissipates at least $E_{\min} = k_B T \ln 2$ as heat.
In this file, Boltzmann's constant $k_B$, room temperature $T = 300$, and the temperature-dependent Landauer energy $E(T) = k_B T \ln 2$ are already defined. The present declaration simply freezes $T$ at the conventional room-temperature value so downstream ratios need not restate the argument.
The broader RS story links erasure to a J-cost paid on the recognition clock τ₀; this constant is the thermodynamic reference against which that cost is compared, not yet the τ₀ derivation itself.
proof idea
Pure definitional abbreviation: apply the already-defined temperature-dependent Landauer energy to the constant room temperature 300. No lemmas, tactics, or arithmetic; the body is the single application landauerEnergy roomTemperature.
why it matters
Gives a named SI-scale anchor for the classical Landauer floor inside the RS information stack. Downstream, efficiencyRatio divides a model current-computer energy by this constant to quantify how far practical erasure sits above the thermodynamic limit ("massive room for improvement").
In the module narrative this supports the INFO-004 target and the paper/patent framing on ultra-low-power computing near the Landauer bound. It does not itself close the τ₀-to-Landauer derivation; it is the fixed-T reference that later J-cost and τ₀ comparisons use.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.