Remark: The proposed protocol interface is not already frozen

An arbitrary sequence of repeated interparty uses, an external unknown quantum message, and a retained quantum receiver port are not specified by ${\mathsf{A}}_0$. A local gate sequence implementing one admitted instrument can be compiled into that instrument; this does not create additional process uses or new event coordinates.

Thus “finite local protocols on the same interface” cannot mean an undeclared enlargement of ${\mathsf{A}}_0$. A transport theorem must state its compatible enlargement and prove the required complete-channel validity.