Target-Family Essence Monotonicity

Abstract

The minimally sufficient joint target becomes finer under family enlargement.

Theorem 1.1 (Joint target minimality and family monotonicity).

$$\begin{array}{r}\forall X:\mathrm{Type},I:\mathrm{Type},B:\mathrm{Type},\\ Y:I\to \mathrm{Type},T:\forall i:I,X\to Y(i),\\ R:X\to B,\\ [((\forall i:I,\mathrm{Refines}(T(i),R))⟺\mathrm{Refines}(\mathrm{jointTarget}(T),R))\wedge \\ (\forall i:I,\mathrm{Refines}(T(i),\mathrm{jointTarget}(T)))\wedge \forall D:\mathrm{Type},q:X\to D,(\forall i:I,\mathrm{Refines}(T(i),q))\Rightarrow \mathrm{Refines}(\mathrm{jointTarget}(T),q)]\wedge \\ (\forall J:\mathrm{Type},Z:J\to \mathrm{Type},A:\forall j:J,X\to Z(j),\mathrm{Refines}(\mathrm{jointTarget}(T),\mathrm{jointTarget}(\mathrm{sumTarget}(T,A)))).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/RefinementAlgebra/TargetFamilyEssenceMonotonicity.multi_target_essence_sufficiency_and_monotonicity (✓ std3). ∎

Source. Repository-derived.

Commentary.

The source’s canonical essence for a target family is the existing jointTarget. A readout decides it exactly when the readout decides every component target.

The joint target decides each component and is coarsest among all simultaneously sufficient concepts. These clauses are supplied by the frozen dependent-family theorem.

The public enlargement clause uses the named sumTarget construction. It adjoins an arbitrary dependent family, and restriction along the left injection proves that the enlarged essence refines the old one.

References

• Truth anchor: D5/S3/ConceptDynamics/RefinementAlgebra/TargetFamilyEssenceMonotonicity.multi_target_essence_sufficiency_and_monotonicity
• Dependency: D5/S3/ConceptDynamics/Refinement/MultiTargetMinimalSufficiency