Theorem: Finite reversible composition

Fix a finite encoding and a prescribed legal word with deterministic canonical code maps and certified finite location transports. There are reversible command circuits $U_1,\dots ,U_L$, fresh retained histories, and reusable clean work such that, at every command boundary,

The decoder ignores implementation histories.

The complete circuits act as the identity on internal matter. For $\rho \in {\mathfrak{S}}_W(c)$, the decoded outputs are the accepted outputs of Theorem C3, with valid original locations. No circuit verifies this semantic membership.

No geometric decoder or admissibility assertion is assigned to arbitrary off-domain words or intermediate synthesis states. Theorem C4's word has the bounds in sec:budget.

Proof. At each boundary, a canonical command has a finite deterministic output map. Flow changes exact parameters and recomputes canonical reports. Incidence changes germ mode, permission, and incidence data. Source replacement evaluates the complete new packet-indexed representation. None of these maps reads internal matter.

Apply lem:completion with stage separation and a fresh geometric history to every command. Earlier histories are acted on by identities. Clean work can be reused after uncomputation.

Location transport is a finite deterministic map conditioned on the geometric input. If it is noninjective, use a separately reserved history of the input location word and the same completion argument. The implementation may consult retained geometric input to execute the already selected location map; this does not make histories accessible source inputs or permit history-dependent geometric decisions.

On eq:composite-domain, each canonical output is in the next command's domain, so decoder correctness follows by induction. Tensoring all code and location gates with the identity on ${\mathcal{H}}_{\Gamma }$ preserves internal matter, including its correlations with untouched references. The semantic promise and Theorem C3 then give the accepted decoded execution.