Mutual Nondisturbance and Observation Order

Abstract

Mutual readout nondisturbance removes observation-order effects.

Theorem 1.1 (Mutual nondisturbance removes order effects).

$$\begin{array}{r}\forall X,C,D:\mathrm{Type},\\ o_C:X\to C,o_D:X\to D,\\ p_C,p_D:X\to X,\\ (o_D\circ p_C=o_D\wedge o_C\circ p_D=o_C)\Rightarrow \\ (\mathrm{forwardJoint}\left(o_C,o_D,p_C\right)=\mathrm{reverseJoint}\left(o_C,o_D,p_D\right))\wedge \\ ((p_D\circ p_C=p_C\circ p_D)\Rightarrow \forall x:X,(\mathrm{forwardJoint}\left(o_C,o_D,p_C,x\right),p_D(p_C(x)))=(\mathrm{reverseJoint}\left(o_C,o_D,p_D,x\right),p_C(p_D(x)))).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/ObservationOrder/MutualNondisturbanceOrderIndependence.mutual_nondisturbance_order_independence (✓ std3). ∎

Source. Repository-derived.

Commentary.

The ordered joint readouts are the canonical forwardJoint and reverseJoint constructions from the ObservationOrder family.

Each update preserves the other instrument’s readout. These two independent equations identify the two joint readout functions.

Under the additional commutation equation, the public second clause compares the complete paired result at every state: its first coordinate is the joint readout and its second is the final state.

References

• Truth anchor: D5/S3/ConceptDynamics/ObservationOrder/MutualNondisturbanceOrderIndependence.mutual_nondisturbance_order_independence
• Dependency: D5/S3/ConceptDynamics/ObservationOrder/PureReadoutOrderIndependence