Basic Dependency Rules

Abstract

Factorization dependence is closed under identity, composition, and joint readouts.

Theorem 1.1 (Concept dependence obeys the basic rules).

$$\begin{array}{c}\forall X,A,B,C,D:\mathrm{Type},\\ q_A:X\to A,q_B:X\to B,\\ q_C:X\to C,q_D:X\to D,\\ \mathrm{Refines}\left(q_A,q_A\right)\wedge \\ (\mathrm{Refines}\left(q_A,\mathrm{conceptJoin}\left(q_A,q_B\right)\right)\wedge \mathrm{Refines}\left(q_B,\mathrm{conceptJoin}\left(q_A,q_B\right)\right))\wedge \\ ((\mathrm{Refines}\left(q_B,q_A\right)\wedge \mathrm{Refines}\left(q_C,q_B\right))\Rightarrow \mathrm{Refines}\left(q_C,q_A\right))\wedge \\ (\mathrm{Refines}\left(q_B,q_A\right)\Rightarrow \mathrm{Refines}\left(\mathrm{conceptJoin}\left(q_B,q_C\right),\mathrm{conceptJoin}\left(q_A,q_C\right)\right))\wedge \\ ((\mathrm{Refines}\left(q_B,q_A\right)\wedge \mathrm{Refines}\left(q_C,q_A\right))\Rightarrow \mathrm{Refines}\left(\mathrm{conceptJoin}\left(q_B,q_C\right),q_A\right))\wedge \\ (\mathrm{Refines}\left(\mathrm{conceptJoin}\left(q_B,q_C\right),q_A\right)\Rightarrow (\mathrm{Refines}\left(q_B,q_A\right)\wedge \mathrm{Refines}\left(q_C,q_A\right)))\wedge \\ ((\mathrm{Refines}\left(q_B,q_A\right)\wedge \mathrm{Refines}\left(q_D,\mathrm{conceptJoin}\left(q_B,q_C\right)\right))\Rightarrow \mathrm{Refines}\left(q_D,\mathrm{conceptJoin}\left(q_A,q_C\right)\right)).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Dependency/BasicDependencyRules.basic_dependency_rules (✓ std3). ∎

Source. Repository-derived.

Commentary.

Identity and composition of factor maps give reflexivity and transitivity. Product projections, paired factor maps, and preservation of a shared coordinate give projection, augmentation, merge, decomposition, and pseudotransitivity.

References

• Truth anchor: D5/S3/ConceptDynamics/Dependency/BasicDependencyRules.basic_dependency_rules
• Dependency: D5/S3/ConceptDynamics/Refinement/RefinementTransitivity