landauerEnergy
plain-language theorem explainer
Defines the Landauer energy of a thermal bath at temperature T as k_B T ln(2), the classical minimum heat cost of erasing one bit. Information and thermodynamics workers in the RS stack cite it as the energy scale feeding positivity, room-temperature evaluation, and the τ₀-normalized erasure-power bound. The body is a three-factor product definition, not a derived equality.
Claim. For a real temperature $T$, the Landauer energy is $E(T) := k_B\, T\, \ln 2$, with Boltzmann constant $k_B = 1.380649\times 10^{-23}\,\mathrm{J/K}$.
background
Module INFO-004 targets the Landauer bound from Recognition Science's fundamental timescale τ₀. Landauer's principle (1961) states that irreversible erasure of one bit dissipates at least $E_{\min} = k_B T \ln 2$ as heat: one bit is $\ln 2$ nats of information, so $\Delta S = k_B \ln 2$ and $Q = T\Delta S$.
In the RS narrative, erasure is framed as recognize-then-forget and therefore carries a J-cost; τ₀ sets the rate at which that thermodynamic cost is paid. The Boltzmann constant used here is the SI value $k_B = 1.380649\times 10^{-23},\mathrm{J/K}$, shared with the computation-limits and Bekenstein–Hawking modules.
This declaration is the bare energy scale. Sibling definitions specialize it (room temperature ≈ 300 K) and divide by τ₀ in seconds to obtain a minimum erasure power.
proof idea
Definitional, not a proof. The body multiplies three reals: the module-local Boltzmann constant, the temperature argument $T$, and $\mathrm{Real.log}, 2$ (natural logarithm). No lemmas are applied; downstream theorems unfold this abbreviation and reason about the factors (positivity of $k_B$, of $T$, and of $\ln 2$).
why it matters
Anchors the classical Landauer scale inside the RS information stack so later results can quote a single named energy. Downstream, positivity of the energy for $T>0$ is proved by unfolding and multiplying positive factors; the room-temperature specialization evaluates the numerical scale $\approx 2.87\times 10^{-21},\mathrm{J}$; and minimum erasure power is this energy divided by τ₀ in seconds.
That power link is the module's stated bridge: τ₀ sets how fast the $k_B T \ln 2$ cost is incurred, connecting thermodynamic Landauer to the recognition timescale and, via siblings, to the J-cost of bit erasure. It does not itself invoke the forcing chain (T5–T8) or the Recognition Composition Law; those enter only if J-cost equality with the thermodynamic expression is discharged later in the file.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.