Pure Readouts and Observation Order

Abstract

Identity observation updates exclude order effects from two static readouts.

Definition 1.1 (An order effect is witnessed at one state).

$$\begin{gathered} \forall X,C,D:\mathrm{Type},forward,reverse:X\to C\times D, \\ \mathrm{hasOrderEffect}(forward,reverse)⟺\exists state:X,forward(state)\ne reverse(state). \end{gathered}$$

Formalization. D5/S3/ConceptDynamics/ObservationOrder/PureReadoutOrderIndependence.hasOrderEffect (✓ std3).

Source. Repository-derived.

Commentary.

For two readouts from X into the same paired output C times D, an order effect holds exactly when some state gives unequal forward and reverse results.

Theorem 1.2 (Pure readouts have no order effect).

$$\forall X,C,D:\mathrm{Type},o_C:X\to C,o_D:X\to D,p_C,p_D:X\to X,E:ApplicationDomain\to \mathrm{Prop},(\forall a:ApplicationDomain,E(a)\Rightarrow \mathrm{hasOrderEffect}(\mathrm{forwardJoint}(o_C,o_D,p_C),\mathrm{reverseJoint}(o_C,o_D,p_D)))\Rightarrow ((p_C=id\wedge p_D=id)\Rightarrow \neg \mathrm{hasOrderEffect}(\mathrm{forwardJoint}(o_C,o_D,p_C),\mathrm{reverseJoint}(o_C,o_D,p_D)))\wedge (\forall a:ApplicationDomain,E(a)\Rightarrow p_C\ne id\vee p_D\ne id).$$

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

Source. Repository-derived.

Commentary.

The forward joint readout observes C, applies its state update, and then observes D. The reverse joint readout observes D first and returns the coordinates in the same C,D order.

An order effect is witnessed by a state where those two paired results differ. Identity updates reduce both constructions to the canonical join of the two static concept readouts.

The public application domain contains quantum measurement, survey order, judicial inquiry, medical diagnosis, psychological priming, and institutional classification. Any reported effect witnessed by the source joint readouts forces at least one nonidentity update.

References

• Truth anchor: D5/S3/ConceptDynamics/ObservationOrder/PureReadoutOrderIndependence.hasOrderEffect
• Truth anchor: D5/S3/ConceptDynamics/ObservationOrder/PureReadoutOrderIndependence.pure_readout_order_independence
• Dependency: D5/S3/ConceptDynamics/ConceptJoinUniversal