Minimal Target-Family Completion

Abstract

Adjoining an entire target family is the coarsest jointly sufficient refinement.

Theorem 1.1 (Target-family completion is coarsest).

$$\begin{array}{c}\forall X,I,Q:\mathrm{Type},Y:I\to \mathrm{Type},\\ q:X\to Q,\\ T:\forall i:I,X\to Y(i),\\ \mathrm{Refines}\left(q,\mathrm{conceptJoin}\left(q,\mathrm{jointTarget}\left(T\right)\right)\right)\wedge \\ (\forall i:I,\mathrm{Refines}\left(T(i),\mathrm{conceptJoin}\left(q,\mathrm{jointTarget}\left(T\right)\right)\right))\wedge \\ \forall D:\mathrm{Type},r:X\to D,\\ \mathrm{Refines}\left(q,r\right)\wedge (\forall i:I,\mathrm{Refines}\left(T(i),r\right))\Rightarrow \\ \mathrm{Refines}\left(\mathrm{conceptJoin}\left(q,\mathrm{jointTarget}\left(T\right)\right),r\right).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Completion/TargetFamilyCompletionMinimality.target_family_completion_is_coarsest (✓ std3). ∎

Source. Repository-derived.

Commentary.

The completion is constructed canonically by joining the current interface with the dependent readout of every target value.

Projection to the first coordinate recovers the current interface. Projection to the joint-target coordinate followed by evaluation recovers every member of the target family.

Any interface that recovers both the current readout and every target receives the paired factor map from this completion. Thus the same construction covers factual, predictive, causal, sequential-effect, indexed-readout, strategy, and self-relevant target families.

References

• Truth anchor: D5/S3/ConceptDynamics/Completion/TargetFamilyCompletionMinimality.target_family_completion_is_coarsest
• Dependency: D5/S3/ConceptDynamics/Refinement/MultiTargetMinimalSufficiency