Canonical Refinement Lowers Conditional Impurity

Abstract

Canonical joint-fiber masses witness impurity monotonicity under refinement.

Theorem 1.1 (Refinement cannot increase conditional impurity).

$$\begin{array}{c}\forall X,C,D,A:\mathrm{Type},\\ mu:\mathrm{PMF}(X),\\ coarse:X\to C,refined:X\to D,\\ target:X\to A,\\ \mathrm{Refines}(coarse,refined)\Rightarrow \\ \mathrm{conditionalLogicalImpurity}(mu,refined,target)\le \mathrm{conditionalLogicalImpurity}(mu,coarse,target).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Information/CanonicalRefinementImpurityMonotonicity.canonical_refinement_impurity_monotone (✓ std3). ∎

Source. Repository-derived.

Commentary.

Each target-conditioned mass is the canonical fiber mass of the joint concept-target readout.

The countable Cauchy inequality compares coarse and refined collision terms; the complementary disagreement identity gives the displayed impurity inequality.

References

• Truth anchor: D5/S3/ConceptDynamics/Information/CanonicalRefinementImpurityMonotonicity.canonical_refinement_impurity_monotone
• Dependency: D5/S3/ConceptDynamics/ConceptJoinUniversal
• Dependency: D5/S3/ConceptDynamics/Information/ConditionalLogicalImpurity