Least Common Readout Refinement

Abstract

The canonical joint readout is the least common refinement and realizes kernel intersection.

Theorem 1.1 (The joint readout is the least common refinement).

$$\begin{array}{c}\forall X,C,D:\mathrm{Type},\\ q_J:X\to C,q_K:X\to D,\\ \mathrm{Refines}\left(q_J,\mathrm{conceptJoin}\left(q_J,q_K\right)\right)\wedge \\ \mathrm{Refines}\left(q_K,\mathrm{conceptJoin}\left(q_J,q_K\right)\right)\wedge \\ (\forall E:\mathrm{Type},q_E:X\to E,\mathrm{Refines}\left(q_J,q_E\right)\Rightarrow \mathrm{Refines}\left(q_K,q_E\right)\Rightarrow \mathrm{Refines}\left(\mathrm{conceptJoin}\left(q_J,q_K\right),q_E\right))\wedge \\ \ker \left(\mathrm{conceptJoin}\left(q_J,q_K\right)\right)=\mathrm{intersection}\left(\ker \left(q_J\right),\ker \left(q_K\right)\right).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Refinement/LeastCommonReadoutRefinement.least_common_readout_refinement (✓ std3). ∎

Source. Repository-derived.

Commentary.

The readouts q_J and q_K share an arbitrary source X. Their joint readout is the canonical conceptJoin, which records the pair of component values without introducing a second join primitive.

The first two public conjuncts are the projection refinements. The third quantifies over every competing readout and states the universal factorization through any common refinement.

The final public conjunct identifies the joint kernel with the intersection of the component kernels. This is the relation used by the repository’s canonical quotient construction.

Both results are direct applications of the frozen concept-family universal property and kernel-order duality theorem.

References

• Truth anchor: D5/S3/ConceptDynamics/Refinement/LeastCommonReadoutRefinement.least_common_readout_refinement
• Dependency: D5/S3/ConceptDynamics/Refinement/ConceptKernelOrderDuality