experimentalStatus
plain-language theorem explainer
Static ledger of three experimental checks on Landauer's principle, each paired with a status string. Anyone citing the RS derivation of the Landauer energy from τ₀ would point here for the empirical side-table. The body is a three-element list literal of named falsifier/status pairs; no proof work.
Claim. The experimental status of Landauer's principle is the finite list of potential falsifiers with recorded outcomes: erasure below $k_B T \ln 2$ (never achieved); information without physical cost (experimentally refuted); reversible near-zero dissipation (achieved in principle).
background
Module INFO-004 derives the Landauer bound from Recognition Science's fundamental timescale $\tau_0$. Classically, erasing one bit costs at least $E_{\min} = k_B T \ln 2$: the heat $Q = T\Delta S$ tied to losing $\ln 2$ nats of information. In RS the same floor is read off the J-cost of a recognize-then-forget cycle, with $\tau_0$ fixing the rate at which that cost is paid.
The sibling structure LandauerFalsifier packages a short name for a potential counterexample together with a status string. Its doc-comment lists four defeat modes: erasure below $k_B T \ln 2$, information without physical cost, perpetual-motion computing, and $\tau_0$ failing to set the fundamental limit. The present definition records the first three as a concrete status table.
proof idea
Definition by list literal. Three structure instances are written out with string fields: "Erasure below limit" / "Never achieved"; "Information without physics" / "Experimentally refuted"; "Reversible near-zero" / "Achieved in principle". No lemmas, tactics, or computation.
why it matters
Closes the empirical side of INFO-004 (Landauer bound from $\tau_0$). The module's core claim is that the thermodynamic floor $k_B T \ln 2$ is forced by the recognition timescale and J-cost; this table states that current evidence does not defeat that claim. It sits next to the quantitative siblings (landauerEnergy, landauer_from_tau0, jcost_equals_thermodynamic, minimumErasurePower) as a human-readable status record rather than a proved inequality. No downstream theorems currently depend on it. Framework contact is the information-thermodynamics bridge, not the T0–T8 forcing chain directly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.