Predictive Memory Monotonicity

Abstract

Predictive memory is monotone under deterministic readout refinement.

Theorem 1.1 (Refinement cannot increase residual predictive memory).

$$\begin{array}{c}\forall P,F,Fine,Coarse,\\ [\mathrm{Fintype}(P)][\mathrm{Fintype}(F)][\mathrm{Fintype}(Fine)][\mathrm{Fintype}(Coarse)],\\ p:P\times F\to \mathbb{R},\\ (\forall z,0\le p(z))\wedge \sum _{z}p(z)=1\Rightarrow \\ \forall qf:P\to Fine,qc:P\to Coarse,\\ \mathrm{Refines}(qc,qf)\Rightarrow \\ \mathrm{predictiveMemory}(p,qf)\le \mathrm{predictiveMemory}(p,qc).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Entropy/Submodularity/PredictiveMemoryMonotonicity.predictive_memory_monotone_under_refinement (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let p be a normalized nonnegative joint mass function on a finite past P and future F. Let qf and qc be deterministic readouts of the same past into finite fine and coarse carriers.

The canonical refinement premise says that qc factors through qf. Thus the coarse readout is obtained from the fine one by a deterministic forgetting map.

The imported refinement decomposition identifies the coarse-minus-fine predictive memory with a nonnegative conditional-information gain. The displayed inequality is its direct monotonicity consequence.

References

• Truth anchor: D5/S3/Entropy/Submodularity/PredictiveMemoryMonotonicity.predictive_memory_monotone_under_refinement
• Dependency: D5/S3/ConceptDynamics/ConceptJoinUniversal
• Dependency: D5/S3/Entropy/Submodularity/RefinementInformationDecomposition