Fixed-Target Completion Flatness

Abstract

Fixed target completions have empty order curvature.

Theorem 1.1 (Fixed target completion has zero curvature).

$$\forall X\in Type,C\in Type,S\in Type,T\in Type,\forall concept\in X\to C,firstTarget\in X\to S,secondTarget\in X\to T,\mathrm{symmDiff}\left(\ker \left(\mathrm{targetClosure}\left(\mathrm{targetClosure}\left(concept,secondTarget\right),firstTarget\right)\right),\ker \left(\mathrm{targetClosure}\left(\mathrm{targetClosure}\left(concept,firstTarget\right),secondTarget\right)\right)\right)=\left\{\right\}$$

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

Source. Repository-derived.

Commentary.

The concept readout and both fixed target maps are independent source primitives. Each completion is the canonical join with the target’s image-valued readout.

The displayed curvature is the symmetric difference of the two kernels, where each kernel is viewed as its exact set of related state pairs.

In either completion order, two states remain equivalent exactly when their original concept values and both fixed target values agree. The two kernel sets therefore coincide.

Repository searches found no exact fixed-target zero-curvature theorem. The proof imports the canonical target-closure construction and applies Mathlib’s symmetric-difference equality criterion.

References

• Truth anchor: D5/S3/ConceptDynamics/Completion/FixedTargetCompletionFlatness.fixed_target_completion_curvature_empty
• Dependency: D5/S3/ConceptDynamics/Completion/TargetClosureOperator