Concept Join Universal Property

Abstract

The product readout is the universal join of two concept readouts.

Definition 1.1 (Refinement is factorization through the finer readout).

$$\begin{gathered} \forall X,C,D:\mathrm{Type},q_C:X\to C,q_D:X\to D, \\ \mathrm{Refines}\left(q_C,q_D\right)⟺\exists factor:D\to C,q_C=factor\circ q_D. \end{gathered}$$

Formalization. D5/S3/ConceptDynamics/ConceptJoinUniversal.Refines (✓ std3).

Source. Repository-derived.

Commentary.

For readouts q_C : X -> C and q_D : X -> D, q_C is refined by q_D exactly when a map from D to C recovers q_C after q_D. The equality is an equality of functions, not merely pointwise implication.

Theorem 1.2 (The product readout is the universal join).

$$\forall X,C,D,E:\mathrm{Type},q_C:X\to C,q_D:X\to D,q_E:X\to E,\mathrm{Refines}\left(q_C,\mathrm{conceptJoin}\left(q_C,q_D\right)\right)\wedge \mathrm{Refines}\left(q_D,\mathrm{conceptJoin}\left(q_C,q_D\right)\right)\wedge \mathrm{Refines}\left(q_C,q_E\right)\Rightarrow \mathrm{Refines}\left(q_D,q_E\right)\Rightarrow \mathrm{Refines}\left(\mathrm{conceptJoin}\left(q_C,q_D\right),q_E\right).$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/ConceptJoinUniversal.concept_join_universal (✓ std3). ∎

Source. Repository-derived.

Commentary.

The joint readout sends x to the pair (q_C x, q_D x). The first two conjuncts factor the component readouts through the product projections.

If both component readouts factor through q_E, pairing their factor maps gives the factor map from q_E to the joint readout. This is the universal property of the concept join.

References

• Truth anchor: D5/S3/ConceptDynamics/ConceptJoinUniversal.Refines
• Truth anchor: D5/S3/ConceptDynamics/ConceptJoinUniversal.concept_join_universal
• Dependency: D5/S3/ConceptDynamics/ConceptFiberDecomposition