Theorem: Derived finite-model acquisition

For the frozen generators and source interface:

1. The scheduled propagators of (eq:kick-H)–(eq:exchange-H) yield (eq:derived-channel). The maps $\mathcal{P},{\Phi }_{\eta },{\mathcal{A}}_{\eta }$ are CPTP.

2. For every finite retained factor $T$, ${{\mathcal{M}}_{\mathcal{B}}}^T={{\mathcal{J}}_{\mathcal{B}}}^T$ on all operators, and

   $${\mathrm{Tr}}_C{{\mathcal{A}}_{\eta }}^T(X)={\mathrm{Tr}}_{J}X.$$

   This includes arbitrary untouched references.

3. Under destructive name semantics, $N,A,E$ are consumed. The newly exported output is the classical record; no measured data name is a quantum output.

Proof. The two summands of $H_{\mathrm{k},k}$ commute, so its propagator is $V_k\otimes {V_k}^{†}$. Since $e^{-i\pi |11⟩⟨11|}=\mathrm{CZ}$, the next propagator is $\mathrm{CZ}$.

On the exchange subspace, ${K_{\mathrm{e}}}^2=I$, whereas it annihilates $00,11$. Thus its propagator satisfies

Taking the environment matrix elements gives $L_0,L_1$. Drawing the independent label $k$, and summing all its unexported branches, yields (eq:derived-channel). Moreover,

The source map is isometric, so these maps are CPTP.

For readout, the Kraus operators are $|r{⟩}_C\otimes D_r$, and their squared moduli sum to $I_B\otimes I_T$. If $X={\sum }_{r,s}|r⟩⟨s{|}_B\otimes X_{rs}$, both readout specifications have $r$-block $X_{rr}$. Therefore the maps agree on all operators, and

Local trace-preserving maps on $J$, followed by local preparation and evolution, preserve the retained marginal. This proves (eq:reference-marginal).

Finally, the name rule removes a measured name from the live quantum context. Enter of $E$ is unexported; Enter of $N,A$ exports two bits. A subsequent unitary preserves live names, classical processing introduces none, and allocation introduces only fresh names. Induction over a continuation proves that no consumed name is reused.