Two logical layers

I: specified semantics. The concrete calculus ${\mathsf{EC}}_{\mathrm{Born}}$ has Born probabilities and destructive projective update by definition. Safety, termination, confluence, adequacy, and no-signaling are theorems about that already specified semantics.

II: unknown measurement. A strategy $\mathsf{S}=(\mathsf{P},\mathsf{U})$ replaces only the measurement transition. The structural class fixes the domain of the characterization. The five requirements

are conditions on the unknown strategy.

The two directions are

The first establishes inhabitation; the second establishes uniqueness within the declared class. A concrete Born calculation is not available for an unknown strategy merely because both strategies interpret the same syntax.