Target Closure Operator

Abstract

Joining a concept with the canonical target readout defines a closure operation.

Theorem 1.1 (Target completion obeys the three closure laws).

$$\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{Refines}\left(q_C,\mathrm{targetClosure}\left(q_C,T\right)\right)\wedge \\ (\mathrm{Refines}\left(q_C,q_D\right)\Rightarrow \mathrm{Refines}\left(\mathrm{targetClosure}\left(q_C,T\right),\mathrm{targetClosure}\left(q_D,T\right)\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/TargetClosureOperator.target_closure_three_laws (✓ std3). ∎

Source. Repository-derived.

Commentary.

Target completion adjoins the canonical target-image readout to a concept readout. Projection onto the original coordinate shows that completion is extensive in the refinement order.

A factor map between two concept readouts lifts to their completions by applying it to the concept coordinate and preserving the shared target coordinate, which proves monotonicity.

Completing twice adds a second copy of the same target coordinate. Duplicating that coordinate and forgetting the duplicate give mutual refinements, so idempotence holds up to concept equivalence despite the changed product codomain.

Lemma 1.2 (Fixed points are exactly target-sufficient concepts).

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

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

Source. Repository-derived.

Commentary.

A concept is unchanged by target completion, up to mutual refinement, exactly when its readout already determines the canonical target readout. In that case adjoining the target adds no distinctions.

Conversely, if completion is equivalent to the original concept, the target projection through the completed readout composes with that equivalence to factor the target through the original concept.

References

• Truth anchor: D5/S3/ConceptDynamics/Completion/TargetClosureOperator.target_closure_equivalent_iff_target_sufficient
• Truth anchor: D5/S3/ConceptDynamics/Completion/TargetClosureOperator.target_closure_three_laws
• Dependency: D5/S3/ConceptDynamics/Disclosure/ExactTargetForcedLeak
• Dependency: D5/S3/ConceptDynamics/Sufficiency/UniversalSufficiencyFactorization