LandauerComputer
plain-language theorem explainer
A three-field record for a physical computer: efficiency as a multiple of the Landauer floor, a technology label, and a flag for Recognition-Science design. Patent-facing data shape for devices that approach $k_B T\ln 2$ erasure cost. Pure structure definition with no proof obligations.
Claim. A Landauer computer is a triple $(e, t, r)$ where $e \in \mathbb{R}$ is the target efficiency as a multiple of the Landauer energy $k_B T \ln 2$, $t$ is a technology label, and $r$ is a Boolean indicating whether the architecture is Recognition-Science designed.
background
Module INFO-004 derives Landauer's bound from Recognition Science's fundamental timescale $\tau_0$. Classically, erasing one bit costs at least $E_{\min} = k_B T \ln 2$: the initial bit is uncertain, the final state is fixed, one nat of information is lost, entropy rises by $k_B \ln 2$, and heat $Q = T\Delta S$ is dissipated.
In RS the same floor is read as a J-cost of "recognize then forget," paid at a rate set by $\tau_0$. Sibling definitions in the module fix $k_B$, room temperature, the Landauer energy, the quantum energy scale from $\tau_0$, minimum erasure power, and the identification of J-cost with the thermodynamic cost.
This structure does not restate that derivation. It packages a device-level claim: how close a concrete machine sits to the bound, what stack it uses, and whether the design is RS-inspired.
proof idea
No proof. The declaration is a structure (record type) with three fields and field doc-comments only. Instantiation is by supplying a real efficiency factor, a technology string, and a Boolean RS-design flag.
why it matters
The module lists four RS predictions: the Landauer bound is exact, reversible computing is in principle energy-free, measurement costs energy because information is created, and $\tau_0$ sets the ultimate speed limit. This structure is the patent-facing carrier for devices that try to approach that bound with RS-inspired architectures (module target: ultra-low-power computing; paper angle: thermodynamics of information from RS).
It sits downstream of the $\tau_0$ and J-cost story rather than of the T0–T8 forcing chain directly. No used_by edges are recorded yet, so it is presently a leaf data shape waiting for concrete device instances and comparison lemmas against landauerEnergy / minimumErasurePower.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.