experimentalVerification
plain-language theorem explainer
Catalog of laboratory confirmations of Landauer's bound: optical-trap erasure (Bérut 2012), feedback-controlled erasure (Jun 2014), and single-atom work (Hong 2016), with present experiments within roughly ten times the thermodynamic floor. Information theorists and RS thermodynamic derivations cite it as the empirical anchor for the τ₀-based Landauer energy. The body is a static string list, not a proof.
Claim. A fixed reference list of experimental reports that Landauer's minimum erasure energy $E_{\min}=k_B T\ln 2$ has been observed in the lab (optical traps, feedback cooling, single-atom systems), currently approached to within a factor of about $10$.
background
Module INFO-004 derives Landauer's principle from Recognition Science's fundamental timescale $\tau_0$ and the $J$-cost of recognition. Classically, erasing one bit raises entropy by $k_B\ln 2$ and therefore dissipates at least $Q=k_B T\ln 2$ as heat. In RS the same floor appears because erasure is a recognize-then-forget cycle whose minimal $J$-cost matches the thermodynamic limit, while $\tau_0$ fixes the rate at which that cost is paid.
Sibling definitions supply the concrete constants: Boltzmann's $k_B$, room temperature, the Landauer energy $k_B T\ln 2$, its positivity, the room-temperature numerical value, $\tau_0$ in seconds, and the identification of erasure $J$-cost with the thermodynamic expression. The present declaration does not recompute those quantities; it only records which experiments have approached the bound.
proof idea
No mathematical argument. The definition is a four-element list of citation strings naming Bérut et al. (2012), Jun et al. (2014), Hong et al. (2016), and a one-line note that the best current experiments sit roughly ten times above the Landauer floor. It is pure bibliographic scaffolding for the surrounding energy and power lemmas.
why it matters
Gives the empirical side of the INFO-004 claim that RS recovers Landauer's bound from $\tau_0$ and $J$-cost. Downstream energy identities (room-temperature Landauer value, minimum erasure power, equality of erasure $J$-cost with $k_B T\ln 2$) can point here when arguing that the derived floor is not merely formal. It does not itself enter the forcing chain (T0–T8) or the Recognition Composition Law; its role is documentary support for the thermodynamics-of-information paper and for ultra-low-power computing claims that approach the Landauer limit. No parent theorems currently depend on it (used_by is empty).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.