Minimal Sufficiency for Multiple Targets

Abstract

The dependent joint target is the coarsest concept sufficient for every target.

Theorem 1.1 (The joint target is minimally sufficient).

$$\begin{array}{c}\forall X,I,B_C:\mathrm{Type},Y:I\to \mathrm{Type},\\ T:\forall i\in I,X\to Y_i,\\ C:X\to B_C,\\ ((\forall i\in I,\mathrm{Refines}\left(T(i),C\right))⟺\mathrm{Refines}\left(\mathrm{jointTarget}\left(T\right),C\right))\wedge \\ (\forall i\in I,\mathrm{Refines}\left(T(i),\mathrm{jointTarget}\left(T\right)\right))\wedge \\ \forall D:\mathrm{Type},q_D:X\to D,(\forall i\in I,\mathrm{Refines}\left(T(i),q_D\right))\Rightarrow \mathrm{Refines}\left(\mathrm{jointTarget}\left(T\right),q_D\right).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Refinement/MultiTargetMinimalSufficiency.multi_target_minimal_sufficiency (✓ std3). ∎

Source. Repository-derived.

Commentary.

For a dependent family of targets, the canonical joint target sends each state to the function listing every target value at that state.

A readout factors every component target exactly when the joint target factors through it. Evaluation at an index gives each component projection from the joint target.

For any simultaneously sufficient candidate, choosing its component factor maps and assembling them pointwise gives a joint readout factorization. This is the stated coarsest-property.

References

• Truth anchor: D5/S3/ConceptDynamics/Refinement/MultiTargetMinimalSufficiency.multi_target_minimal_sufficiency
• Dependency: D5/S3/ConceptDynamics/ConceptJoinUniversal