Proposition: Decoder-correct event permutation

Exchange every valid forward input in eq:encodedmap with its specified output and fix every other basis string. This defines a permutation $U_B$ of the full finite code space. On its declared forward precondition,

This includes geometry, permission, germ incidence, and original location transport. History is returned as storage. The square has an analogous permutation $U_A$.

Proof. Injectivity and disjoint modes make the exchanged pairs disjoint. At $j=0$, central reports are zero, arm formulas agree, and all peripheral formulas coincide. Hence unchanged reports are valid. Mode selects the outgoing germ, permission decreases, tables remain fixed, and locations become exactly $\tau (x)$.

The decoder ignores returned implementation history but does not discard its wires. Report words are not promoted to new exact lengths.