Concept Entropy under Refinement

Abstract

Refinement increases concept information and decreases residual entropy.

Theorem 1.1 (Refinement increases information and decreases residual entropy).

$$\begin{array}{c}\forall X,C,D,\\ [\mathrm{Fintype}(X)][\mathrm{Fintype}(C)][\mathrm{Fintype}(D)],\\ mu:X\to \mathbb{R},\\ q_C:X\to C,q_D:X\to D,\\ ((\forall x,0\le mu(x))\wedge \sum _{x}mu(x)=1)\wedge \mathrm{Refines}(q_C,q_D)\Rightarrow \\ (\mathrm{conceptInformation}(mu,q_C)\le \mathrm{conceptInformation}(mu,q_D))\wedge \\ (\mathrm{conceptResidual}(mu,q_D)\le \mathrm{conceptResidual}(mu,q_C)).\end{array}$$

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

Source. Repository-derived.

Commentary.

Let mu be a normalized nonnegative mass function on a finite state carrier. Concept information is the Shannon entropy of the readout pushforward, while concept residual is the conditional entropy of the source state given that readout.

Both laws are constructed from mu and the canonical concept readouts. Refinement uses the family factorization relation: the coarse readout is obtained by deterministically forgetting the fine one.

The displayed information and residual inequalities are separate public conjuncts. The proof directly applies the frozen deterministic pushforward entropy classification and then the finite entropy chain rule to the graph-supported readout laws.

References

• Truth anchor: D5/S3/ConceptDynamics/Information/RefinementEntropyMonotonicity.refinement_information_residual_monotone
• Dependency: D5/S3/ConceptDynamics/ConceptJoinUniversal
• Dependency: D5/S3/Entropy/Forgetting/DeterministicEntropyEquality