Refinement Lowers Conditional Logical Impurity

Abstract

Factor-map refinement cannot increase conditional logical impurity.

Theorem 1.1 (Refinement cannot increase 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/RefinementImpurityMonotonicity.refinement_impurity_monotone (✓ std3). ∎

Source. Repository-derived.

Commentary.

A coarse concept fiber is the union of the refined fibers selected by the refinement factor map.

The countable Cauchy inequality bounds each coarse target-collision term by the corresponding refined terms. The complementary pair-disagreement normalization then reverses this comparison for conditional logical impurity.

References

• Truth anchor: D5/S3/ConceptDynamics/Information/RefinementImpurityMonotonicity.refinement_impurity_monotone
• Dependency: D5/S3/ConceptDynamics/ConceptJoinUniversal
• Dependency: D5/S3/ConceptDynamics/Information/ConditionalLogicalImpurity