D2: record pullback versus instrument compatibility

This is the finite pullback criterion recorded in En03-A CheungEn03A (theorem :pullback). It determines effects, not complete selective maps.

For instruments $({\Phi }_w{)}_w$ and $({\Psi }_w{)}_w$ with identified residual output spaces, full implementation compatibility is instead

Equality on all matrix units certifies this map identity and therefore also equality with every untouched reference. Its trace consequence is record compatibility, but the converse fails.