Theorem: Explicit batch recovery and its ledger

The programme

implements

and satisfies $\mathcal{D}{\mathcal{N}}_A={\mathrm{id}}_2$, including every reference.

Its resource vector has

It allocates no ancilla and is peak-optimal for batch access.

Proof. Destructively measuring $F$ and summing its outcomes is precisely the partial trace over $F$. Equation (eq:normalform) proves recovery. Alternatively, (eq:factor) proves it before tracing and therefore with every reference.

The syndrome outcomes are uniform over four values and independent of the logical-reference state. Each normalized positive branch returns the original logical state with its reference correlations.

Three input names are initially live. Gates preserve that count. The two readout names are then consumed, leaving one returned qubit. The two readouts share the eighth round. No quantum record or environment remains unconsumed. Batch access forces the initial lower bound three.