Coordinate-Deletion Robustness

Abstract

One more separating coordinate than the deletion budget preserves joint faithfulness.

Theorem 1.1 (Redundant separation survives bounded coordinate deletion).

$$\begin{array}{r}\forall I,X:\mathrm{Type},O:I\to \mathrm{Type},\\ q:\forall i:I,X\to O(i),f\in \mathbb{N},\\ (\forall x,y:X,x\ne y\Rightarrow (\exists S:\mathrm{Finset}\left(I\right),\mathrm{card}\left(S\right)=f+1\wedge \forall i:S,q\left(i,x\right)\ne q\left(i,y\right)))\Rightarrow \\ \forall D:\mathrm{Finset}\left(I\right),\mathrm{card}\left(D\right)\le f\Rightarrow \\ \mathrm{Injective}\left(\mathrm{jointReadout}\left(\mathrm{restrict}\left(q,\{i:I\mid \neg (i\in D)\}\right)\right)\right).\end{array}$$

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

Source. Repository-derived.

Commentary.

For every distinct pair of states, the premise supplies a finite set of exactly f + 1 coordinates whose readouts separate that pair. This witness form states the source’s at-least condition without requiring decidable equality on any output carrier.

A deleted coordinate set of cardinality at most f cannot contain the entire separating witness. Evaluating equal surviving joint readouts at a witness outside the deleted set contradicts its separation property.

The conclusion uses the existing dependent jointReadout on the subtype of coordinates outside the deleted set, so completeness is injectivity of the canonical surviving observation family.

References

• Truth anchor: D5/S3/ConceptDynamics/Faithfulness/CoordinateDeletionRobustness.coordinate_deletion_robustness
• Dependency: D5/S3/ConceptDynamics/Faithfulness/JointFaithfulnessLeibnizCriterion