Proposition: Record versus residual criterion

The two instruments have equal record laws on every input exactly when

Their recorded residual expectations agree on a declared algebra $\mathcal{O}$ exactly when

The corresponding map identities remain valid under untouched reference extension.

Proof. Pair an output record block first with $I$, then with $B$, and pull the effect back to the input. Equality against every density matrix is equality of the Hermitian effects; complex linearity gives the full identities. Reference extension tensors the resulting linear-map equalities with identity.