quantum_is_reversible
plain-language theorem explainer
Unitary quantum evolution preserves information and is therefore reversible; only measurement (projection) is irreversible and incurs an energy cost. Anyone linking Landauer erasure to quantum computation in the RS information stack would cite this marker. The proof is the trivial inhabitant of True: a documented placeholder, not an operator-algebra argument.
Claim. Unitary quantum operations preserve information (they are reversible). Measurement is irreversible and dissipates energy. Formally the claim is recorded as the proposition $\mathrm{True}$.
background
Module INFO-004 derives the Landauer bound $E_{\min}=k_B T\ln 2$ from Recognition Science's fundamental timescale $\tau_0$ and the $J$-cost. Landauer's principle says erasing one bit costs at least that heat; in RS the same bound is read as ledger accounting: information is ledger entries, erasure removes an entry, and double-entry balance forces a minimum transaction fee equal to the thermodynamic limit.
The surrounding siblings define $k_B$, room-temperature Landauer energy, $\tau_0$ in seconds, a quantum energy scale, minimum erasure power, and the identification of erasure $J$-cost with the thermodynamic cost. Upstream ledger and cost infrastructure (double-entry ledgers, multiplicative-recognizer cost, rung-coarsened recognition cost) supplies the accounting language; this declaration only records the standard quantum dichotomy that unitaries preserve information while measurement does not.
proof idea
Term-mode proof: the goal is literally True, discharged by trivial. No lemmas about unitaries, completely-positive maps, or von Neumann entropy are invoked. The inline comments state the intended physics (unitaries preserve information; measurement is irreversible and costs energy) but are not part of the formal obligation.
why it matters
Sits in the Landauer-from-$\tau_0$ development as a conceptual hinge: reversible quantum gates do not pay the Landauer fee; irreversible erasure and measurement do. That split matches the module's RS reading of Landauer as a ledger transaction fee for deleting entries, and it frames why the bound is about forgetting rather than about coherent evolution. No downstream theorems currently depend on it (used_by is empty), so it functions as a named marker inside INFO-004 rather than a load-bearing lemma in the forcing chain (T0–T8) or the Recognition Composition Law. It does not yet connect $\hbar=\phi^{-5}$ or the eight-tick register to a concrete unitary group on the recognition Hilbert space.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.