Faithful Observation Commutation Criterion

Abstract

Jointly faithful observations detect equality of two process orders.

Theorem 1.1 (Faithful observations detect commutation).

$$\begin{array}{r}\forall I,X:\mathrm{Type},Output:I\to \mathrm{Type},\\ Q:\forall i:I,X\to \mathrm{Output}\left(i\right),\\ Fu,Fv:X\to X,\\ \mathrm{Injective}\left(\mathrm{jointReadout}\left(Q\right)\right)\wedge \\ (\forall i:I,x:X,Q\left(i,\mathrm{apply}\left(Fu,\mathrm{apply}\left(Fv,x\right)\right)\right)=Q\left(i,\mathrm{apply}\left(Fv,\mathrm{apply}\left(Fu,x\right)\right)\right))⟹\\ Fu\circ Fv=Fv\circ Fu.\end{array}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Faithfulness/FaithfulObservationCommutationCriterion.faithful_observation_commutation_criterion (✓ std3). ∎

Source. Repository-derived.

Commentary.

The dependent family is assembled with the canonical jointReadout. Coordinatewise agreement of the two composite states therefore becomes equality of their joint readings.

Injectivity identifies those states for every input, and function extensionality identifies the composite processes.

References

• Truth anchor: D5/S3/ConceptDynamics/Faithfulness/FaithfulObservationCommutationCriterion.faithful_observation_commutation_criterion
• Dependency: D5/S3/ConceptDynamics/Faithfulness/JointFaithfulnessLeibnizCriterion