Proposition: Semantic scope

Under Assumption ass:I, the ideal finite program reads the $b_N$ carrier qubits destructively, retains their raw tuple, applies the total decoder, and returns untested spectators with the channel (eq:idealread). The specified finite pointer instrument has the corresponding ordinary Born interpretation.

Proof. For pure finite-register inputs the characterization gives the displayed measurement maps. Sequential reads compose to $⟨j{|}_Q$. A finite mixed carrier–spectator state has a finite purification; embed its purifying space into qubits, apply the pure-state statement, and trace out the ancillary factors. The result is $M_{j}X{M}_j^{†}$, independent of the chosen purification. Pointer allocation, finite interactions, readout, and classical assignment compose the same way.