Theorem: B1: resource-certified decoder soundness

Under specified Born semantics, a finite legal programme with the above certificate implements its declared channel on arbitrary reference-entangled inputs and obeys its declared peak bound.

Proof. Along a history, compose allocation isometries, gates, and destructive measurement bras. The resulting linear map is $K_h$. Branch normalizations cancel against the product of branch probabilities, leaving the unnormalized output $K_h\rho {K_h}^{†}$.

Completeness follows by backward induction on the finite instruction tree. Gates and allocations are isometric. At a readout, ${\sum }_{\kappa }{M_{\kappa }}^{†}{M}_{\kappa }=I$. Every subsequent branch is complete by induction, so

The programme therefore defines a CPTP output channel, or a complete instrument if outcomes are reported.

Equality of Choi blocks is equality on all matrix units and hence equality of the linear maps. Tensoring this equality with ${\mathrm{id}}_R$ proves correctness with every reference.

Finally, the live-name ledger counts every allocated, surviving, and returned quantum factor on each branch. Its maximum is the claimed bound by Definition def:peak. Consumption and return ensure there is no unpriced quantum output.