Definition: Resource-certified programme

A certificate for $\pi$ comprises:

1. its finite instruction tree and its input/output names;

2. the branch path maps $K_h$;

3. the complete selective channel

   $${{\Phi }_y}^{\pi }(\rho )=\sum _{h:\mathrm{out}(h)=y}{K}_h\rho {K_h}^{†};$$

4. an equality of the task channel composed with ${\mathcal{N}}_A$, certified on all matrix units;

5. a live-name ledger at every instruction and branch.

All outcomes are retained in the branch sum. A successful branch alone is not a deterministic recovery.