Target Closure Reflection

Abstract

Target closure is the least target-sufficient refinement and reflects into the target-sufficient concepts.

Lemma 1.1 (Target sufficiency is constancy on concept fibers).

$$\begin{array}{c}\forall X,D,Y:\mathrm{Type},\\ \mathrm{Nonempty}\left(X\right),q_D:X\to D,T:X\to Y,\\ \mathrm{TargetSufficient}\left(q_D,T\right)⟺\forall x,y:X,q_D(x)=q_D(y)\Rightarrow T(x)=T(y).\end{array}$$

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

Source. Repository-derived.

Commentary.

On a nonempty state space, a concept is target-sufficient exactly when the target takes the same value on every pair of states that the concept readout identifies.

Equivalently, the canonical target-image readout factors through the concept precisely when the target is constant on each concept fiber.

Theorem 1.2 (Target closure has the reflection universal property).

$$\begin{array}{c}\forall X,B,D,Y:\mathrm{Type},\\ q_C:X\to B,q_D:X\to D,T:X\to Y,\\ \mathrm{TargetSufficient}\left(q_D,T\right)\Rightarrow (\mathrm{Refines}\left(\mathrm{targetClosure}\left(q_C,T\right),q_D\right)⟺\mathrm{Refines}\left(q_C,q_D\right)).\end{array}$$

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

Source. Repository-derived.

Commentary.

Fix a target-sufficient comparison concept. The target closure of a concept refines that comparison exactly when the original concept already refines it.

One direction follows because the original concept refines its closure. For the other, the comparison receives both the original concept and the canonical target readout, so the universal property of their join supplies the required factorization.

Lemma 1.3 (Target closure is the least target-sufficient refinement).

$$\begin{array}{c}\forall X,B,Y:\mathrm{Type},\\ q_C:X\to B,T:X\to Y,\\ \mathrm{TargetSufficient}\left(\mathrm{targetClosure}\left(q_C,T\right),T\right)\wedge \\ \mathrm{Refines}\left(q_C,\mathrm{targetClosure}\left(q_C,T\right)\right)\wedge \\ \forall D:\mathrm{Type},q_D:X\to D,\\ (\mathrm{TargetSufficient}\left(q_D,T\right)\wedge \mathrm{Refines}\left(q_C,q_D\right))\Rightarrow \mathrm{Refines}\left(\mathrm{targetClosure}\left(q_C,T\right),q_D\right).\end{array}$$

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

Source. Repository-derived.

Commentary.

Target closure is itself target-sufficient and refines the original concept by adjoining only the canonical target coordinate.

Every target-sufficient concept that refines the original concept also receives a factor map from the closure. These three properties make the closure the least target-sufficient refinement in the concept refinement order.

Lemma 1.4 (Target closure is a target-sufficient fixed point).

$$\begin{array}{c}\forall X,B,Y:\mathrm{Type},\\ q_C:X\to B,T:X\to Y,\\ \mathrm{TargetSufficient}\left(\mathrm{targetClosure}\left(q_C,T\right),T\right)\wedge \\ \mathrm{ConceptEquivalent}\left(\mathrm{targetClosure}\left(\mathrm{targetClosure}\left(q_C,T\right),T\right),\mathrm{targetClosure}\left(q_C,T\right)\right).\end{array}$$

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

Source. Repository-derived.

Commentary.

Completing a concept makes the target recoverable from its readout. Completing the result again adds no new distinctions: the twice-completed readout and the once-completed readout mutually refine one another.

Thus target closure lands among the target-sufficient concepts and is idempotent there up to concept equivalence.

Lemma 1.5 (Target sufficiency is necessary for the reflection equivalence).

$$\begin{array}{c}\exists q_C,q_D:\mathrm{Concept}\left(Bool,Unit\right),\\ \neg \mathrm{TargetSufficient}\left(q_D,i{d}_{Bool}\right)\wedge \\ \mathrm{Refines}\left(q_C,q_D\right)\wedge \\ \neg \mathrm{Refines}\left(\mathrm{targetClosure}\left(q_C,i{d}_{Bool}\right),q_D\right).\end{array}$$

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

Source. Repository-derived.

Commentary.

Take both concepts to be the constant readout from the two Boolean states to the one-point type, and take the target to be the Boolean identity. The two concepts refine one another, but neither can recover the target.

The target closure records the Boolean target coordinate and therefore distinguishes false from true. It cannot factor through the one-point comparison concept, which witnesses failure of the reflection equivalence when target sufficiency is omitted.

References

• Truth anchor: D5/S3/ConceptDynamics/Completion/TargetClosureReflection.target_closure_is_least_target_sufficient_refinement
• Truth anchor: D5/S3/ConceptDynamics/Completion/TargetClosureReflection.target_closure_is_target_sufficient_fixed_point
• Truth anchor: D5/S3/ConceptDynamics/Completion/TargetClosureReflection.target_closure_reflection_universal
• Truth anchor: D5/S3/ConceptDynamics/Completion/TargetClosureReflection.target_sufficiency_hypothesis_is_necessary
• Truth anchor: D5/S3/ConceptDynamics/Completion/TargetClosureReflection.target_sufficient_iff_fiber_constant
• Dependency: D5/S3/ConceptDynamics/Completion/TargetClosureOperator