Local-Global Residual Criterion

Abstract

The dependent residual of distinct states invisible to every local readout is empty exactly when the joint readout is injective.

Theorem 1.1 (Residual emptiness is joint injectivity).

$$\begin{array}{r}\forall I,X:\mathrm{Type},V:I\to \mathrm{Type},\\ q:\forall i:I,X\to V\left(i\right),\\ \mathrm{IsEmpty}\left(\{(x,y):X\times X\mid x\ne y\wedge \forall i:I,q\left(i,x\right)=q\left(i,y\right)\}\right)⟺\mathrm{Injective}\left(\mathrm{jointReadout}\left(q\right)\right).\end{array}$$

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

Source. Repository-derived.

Commentary.

For an indexed dependent family q_i : X -> V_i, the residual is the dependent type of pairs of distinct states whose readings agree at every index.

Emptiness of this residual says that coordinatewise equality separates states. The canonical jointReadout packages exactly those coordinate values, so the frozen joint-faithfulness criterion identifies this separation property with injectivity.

References

• Truth anchor: D5/S3/ConceptDynamics/Faithfulness/LocalGlobalResidualCriterion.local_global_residual_empty_iff_joint_injective
• Dependency: D5/S3/ConceptDynamics/Faithfulness/JointFaithfulnessLeibnizCriterion