Lemma: Decoder-correct reversible implementation

The finite map (eq:event-code) has a permutation extension to the complete binary code space. That permutation has an exact NOT–CNOT–Toffoli implementation with clean work uncomputed. It acts as the identity on internal matter.

Proof. The output history determines $x$, and its permission determines $k$, so the forward map is injective. Input and output sets are disjoint because their modes differ. Exchange each valid input with its designated output, and fix all other strings. The exchanges are disjoint transpositions. The decoder reads exactly the outgoing germ, spent permission, and transported locations.

For completeness, any transposition of two $N$-bit strings can be synthesized along a Gray path between them. The symmetric sequence of adjacent transpositions exchanges the endpoints and fixes intermediate strings. An adjacent transposition is a NOT on the differing bit, controlled on all other bits. Negative controls are converted by NOT gates; the conjunction of positive controls is computed with Toffoli gates into clean work, used once, and uncomputed. Apply this construction to the finite transposition list. History is deliberately retained; it is not clean work.