Definition: Local replacement on a common skeleton

Two circuits form a $K$-local replacement pair if they have the same typed skeleton, source and output placements, transport connections, and unchanged resources, and their vertex channels differ only at vertices supported in the compact set $K$.

An initial-input modification confined to $K$ means equality of the joint reductions on all external input factors outside $K$, including any untouched reference being compared.