Theorem: Finite-circuit adequacy

Every well-typed program with a first-order interface denotes a finite quantum instrument. Conversely, every finite circuit built from the available gates, zero-state allocation, destructive computational-basis readout, and finite classical control has a well-typed implementation with the same instrument.

Proof. For reported output $y$, define

The maps are completely positive and their sum is trace preserving by Lemma lem:path. Unrolling the finite formal evaluation tree gives a finite adaptive circuit.

Conversely, input wires are linear arguments. Fresh wires use $\mathsf{new}$, routing uses pairing and tuple elimination, and operations use gates or $\mathsf{Enter}$. Finite control uses conditionals, $\mathsf{copyBit}$, and $\mathsf{dropBit}$. Every quantum wire is passed to exactly one next operation, explicitly consumed, or returned. Induction through the circuit identifies its path maps.