Target Recovery Criterion

Abstract

A process preserves a target exactly when it creates no target-sensitive fiber defect.

Theorem 1.1 (Recovery is equivalent to absence of a target defect).

$$\begin{gathered} \forall X,Y,Z:\mathrm{Type}, \\ [\mathrm{Nonempty}(X)],U:X\to Y,T:X\to Z, \\ (\exists r:Y\to Z,T=r\circ U\iff \forall x,y:X,U(x)=U(y)\Rightarrow T(x)=T(y))\wedge \\ (\forall x,y:X,U(x)=U(y)\Rightarrow T(x)=T(y)\iff \mathrm{defectRelation}\left(U,T\right)=\varnothing )\wedge \\ (\mathrm{defectRelation}\left(U,T\right)=\varnothing \iff \exists r:Y\to Z,T=r\circ U)\wedge \\ (\neg (\exists r:Y\to Z,T=r\circ U)\iff \mathrm{Nonempty}\left(\mathrm{defectRelation}\left(U,T\right)\right)). \end{gathered}$$

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

Source. Repository-derived.

Commentary.

Let U be a process readout and T the target to recover. The inhabited state premise supplies a target value for extending a factor map to process outputs outside the realized range.

The defect relation is constructed from U and T. It contains exactly the pairs merged by U but separated by T, so its nonemptiness is the public witness that recovery fails.

The accepted answerability criterion supplies all three positive equivalences and directly applies the pinned whole-codomain factorization theorem. Negating its empty-defect equivalence gives the final merged-state characterization.

References

• Truth anchor: D5/S3/ConceptDynamics/Restoration/TargetRecoveryCriterion.target_recovery_criterion
• Dependency: D5/S0/Rewriting/Quotients/AnswerabilityCriterion
• Dependency: D5/S3/ConceptDynamics/TargetRisk/RefinementRiskCostTradeoff