reversible_approaches_zero
plain-language theorem explainer
In principle, reversible computation can dissipate arbitrarily little energy per logical step; only finite speed and error correction impose practical floors. Information theorists and RS thermodynamics readers cite this as the qualitative counterpart to the Landauer erasure bound. The proof is the trivial inhabitant of True, recording the claim as an accepted principle rather than a derived inequality.
Claim. In the ideal limit, reversible computation may use arbitrarily little energy. Practical lower bounds arise only from finite operating speed and the overhead of error correction, not from logical irreversibility itself.
background
Module INFO-004 derives Landauer's bound from Recognition Science's fundamental timescale $\tau_0$. Landauer (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 J-cost of recognizing then forgetting a bit, with $\tau_0$ setting the rate at which that cost is paid.
Reversible computing is the complementary regime: when no information is erased, the thermodynamic argument does not force a positive energy floor. The classical and quantum pictures agree that unitary (hence reversible) gates can, in the slow, error-free limit, approach zero dissipation per operation. Sibling declarations in the module fix $k_B$, room temperature, the Landauer energy, and the identification of erasure J-cost with the thermodynamic heat $k_B T \ln 2$.
proof idea
Term-mode proof of True by trivial. No lemmas are applied; the declaration is an explicit principle marker, not an inequality derivation. Comments in the signature record the intended reading (arbitrarily little energy in theory; finite speed and error correction in practice).
why it matters
Places the reversible-computing zero-dissipation ideal next to the Landauer erasure bound inside the RS information stack. The module target is to obtain $E_{\min} = k_B T \ln 2$ from $\tau_0$ and J-cost; this theorem marks the contrasting regime in which no bit is erased, so the Landauer floor need not apply. No downstream theorems currently depend on it. It does not touch the forcing chain (T0–T8), RCL, or the $\phi$-ladder mass formula; it is local to INFO-004 thermodynamics-of-information narrative and the ultra-low-power computing motivation stated in the module doc.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.