PM-DRV-0030

A Derivation SHOULD write the Properties that the target State's Restriction requires, so that on completion the transitioning object satisfies that Restriction.

Non-normative, and this is the most quietly important sentence in the whole source material. It ties the three constructs together into something checkable: the target State has a Restriction, the Derivation writes data, and the claim is that the data the Derivation writes entails the Restriction.

That is a proof obligation, and it can be discharged mechanically rather than trusted. For each Operation:

restriction(source) ∧ filters ∧ conditions ∧ derived-data ⊨ restriction(target)

If it cannot be discharged, the Operation does not have a guaranteed outcome and the model is under-specified — which is something a tool can refuse to release rather than something a user discovers in production. Stated as PO-0001.

The level here is SHOULD rather than MUST because the source says "guaranteed by deriving a value" descriptively, about one example, rather than stating it as a rule. Whether it is intended as a universal requirement is Q-G-0016.