Indexed Target Sufficiency

Abstract

An indexed local readout is target-sufficient exactly when its complete readout has no target-sensitive defect.

Theorem 1.1 (Target stability, recovery, and empty defect are equivalent).

$$\begin{array}{r}\forall I,X,T:\mathrm{Type},O:I\to \mathrm{Type},\\ \mathrm{Nonempty}\left(X\right),q:\forall i:I,X\to O(i),t:X\to T\Rightarrow \\ q_{all}=\mathrm{jointReadout}\left(q\right),\\ (\mathrm{defectRelation}\left(q_{all},t\right)=\varnothing \iff \forall x,y:X,(\forall i:I,q\left(i,x\right)=q\left(i,y\right))\Rightarrow t(x)=t(y))\wedge \\ ((\forall x,y:X,(\forall i:I,q\left(i,x\right)=q\left(i,y\right))\Rightarrow t(x)=t(y))\iff \exists r:\prod _{i:I}O(i)\to T,t=r\circ q_{all})\wedge \\ (\mathrm{defectRelation}\left(q_{all},t\right)=\varnothing \iff \exists r:\prod _{i:I}O(i)\to T,t=r\circ q_{all})\wedge \\ \exists q0:\forall i:Unit,Bool\to Unit,t0:Bool\to Unit,\\ \mathrm{defectRelation}\left(\mathrm{jointReadout}\left(q0\right),t0\right)=\varnothing \wedge \exists r:(Unit\to Unit)\to Unit,t0=r\circ \mathrm{jointReadout}\left(q0\right)\wedge \neg \mathrm{Injective}\left(\mathrm{jointReadout}\left(q0\right)\right).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Restoration/IndexedTargetSufficiency.indexed_target_sufficiency (✓ std3). ∎

Source. Repository-derived.

Commentary.

The complete readout is constructed from the indexed local channels by collecting every coordinate into one dependent tuple. Its target defect contains exactly the state pairs that all channels merge while the target separates them.

On an inhabited state space, the accepted recovery criterion supplies a factor on the full dependent output type. Function extensionality identifies equality of complete readouts with coordinatewise local equivalence.

The final public witness uses the same constant local readout and constant target for its empty defect, recovery factor, and failure of state injectivity. It therefore shows that task sufficiency does not require recovering complete identity.

References

• Truth anchor: D5/S3/ConceptDynamics/Restoration/IndexedTargetSufficiency.indexed_target_sufficiency
• Dependency: D5/S3/ConceptDynamics/Faithfulness/JointFaithfulnessLeibnizCriterion
• Dependency: D5/S3/ConceptDynamics/Restoration/TargetRecoveryCriterion