Explicit programs and their output ledgers

For a finite proxy, let $Q_C,Q_R,Q_B$ denote qubit dictionaries for the logical code and the two outputs. These are register abbreviations, with encoded-subspace conditions understood. Let $U_{\mathrm{body},t}$ be a specified padded unitary whose restriction implements the prepared proxy isometry.