Manuscript VII-E@1 · VII-E.tex · lemma · b713cf3c
Lemma: Injectivity with retained history
One certified four-face slicing exchange › Finite code and reversible implementation · lines 2488–2497 · proof included or linked
VII-E@1#lem:event-injection
The map eq:event-code-map is injective, and its input and output sets are disjoint.
Proof. The output history determines , and the output permission determines . All other words are retained. Input and output modes differ.