Lemma: Finite path semantics

For a fixed well-typed program with a first-order interface, every complete classical history $h$ determines a linear map $K_h$ from its quantum input space to its returned quantum output space. It is a composition of allocation isometries, gates, wiring permutations, and destructive readout maps. For a pure input $\psi$,

and

Proof. A complete history fixes all classical choices. Administrative reductions determine syntax and wiring but do not inspect the quantum vector. Multiplying the quantum maps along the history gives $K_h$. The successive conditional normalizations cancel in the product of branch probabilities, leaving ${\Vert K_h\psi \Vert }^2$.

For completeness use the finite formal outcome tree, including branches whose weight is zero on a particular input. At a readout,

Allocation is isometric and gates are unitary. Backward induction on the tree proves completeness. All paths have the same output Hilbert space after the canonical identification by the returned tuple.