Proposition: Decoder-correct finite permutation

Exchange each valid input in eq:event-code-map with its specified output, and fix every other basis string. This defines a permutation $U_{\mathrm{ex}}$ of the complete finite code space. On the declared forward domain,

The decoded equality includes geometry, permission, event germ, and original-name locations. History remains an output of the implementation.

Proof. By lem:event-injection, all exchanged pairs are disjoint. Their exchanges and the identity on the remaining strings form a permutation.

At $j=0$, both central lengths are zero; the two arm formulas agree; and every peripheral formula is identical on the two germs. Hence the unchanged report words remain valid. The mode selects outgoing incidence, permission decreases, all fixed chart data remain unchanged, and the location tuple becomes $\tau (x)$. These are precisely the semantic event outputs.

Ignoring history in the geometric decoder does not discard it from the circuit interface.