ReversibleComputation
plain-language theorem explainer
Reversible computation is packaged as invertibility of every step plus absence of bit erasure; those two flags jointly force zero dissipation in principle. Information theorists and RS workers on the Landauer bound cite it as the zero-cost side of the ledger against erasure. It is a plain structure definition whose third field is the conjunction of the first two.
Claim. A reversible computation is specified by two Boolean flags: every operation is invertible, and no bits are erased. Dissipation is zero in principle precisely when both flags hold, i.e. when the computation is invertible and erasure-free.
background
Module INFO-004 derives Landauer's bound from Recognition Science's fundamental timescale $\tau_0$. Landauer's principle (1961) states that erasing one bit costs at least $E_{\min} = k_B T \ln 2$ in heat. In RS the same floor is read off the $\tau_0$ clock and the $J$-cost of "recognize then forget."
The complementary case is computation that never erases. If every step is invertible and no bit is discarded, the Landauer tax is not incurred. The structure records exactly those two conditions and packages their conjunction as the zero-dissipation claim.
Sibling material in the module fixes $k_B$, room temperature, the Landauer energy, the link from $\tau_0$ to that energy, and the identification of erasure $J$-cost with the thermodynamic expression.
proof idea
No proof body: this is a structure definition. The fields invertible and no_erasure are Booleans; zero_dissipation is defined to be their conjunction. Instantiating the structure is just supplying the two flags and obtaining the derived zero-dissipation proposition for free.
why it matters
In the Landauer module this structure is the formal zero-cost pole: reversible, erasure-free computation approaches zero energy in principle, against which the positive Landauer floor for erasure is measured. The module doc flags patent and paper interest in ultra-low-power computing that approaches the Landauer limit; this definition is the clean side of that contrast.
It sits next to the $\tau_0$-derived energy, the room-temperature Landauer value, and the equality of erasure $J$-cost with the thermodynamic $k_B T \ln 2$ expression. No downstream theorems currently depend on it in the graph, so it functions as a local interface for later reversible-computing arguments rather than a proved forcing-chain step (T0–T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.