Programme soundness and resource accounting

This is the finite execution interface of En02-B/C, reproved for the stated programme class CheungEn02B,CheungEn02C.

The decoder's quantum peak is at most $s+2$ qubits: $s$ label qubits and two coefficient legs arrive at the receiver. After destructive label readout, two quantum legs remain; after discard, one is returned. Classical label storage is a separate ledger.

The inaccessible supplier holds $h$ gauge qubits. A Choi validation experiment additionally uses $h+1$ input-reference qubits. Those references are not available to the decoder and are not omitted from a whole-experiment ledger.

The exact finite gate library includes the printed $F_d$. No laboratory synthesis, optimal gate count, or resource-optimal compiler is inferred.