Selected Observation Information Monotonicity, Canonical Form

Abstract

Selected canonical joint readouts carry monotone mutual information.

Theorem 1.1 (Selected canonical readout information is monotone).

$$\begin{array}{c}\forall Sample:\mathrm{Type},Hidden:\mathrm{Type},Index:\mathrm{Type},\\ Output:Index\to \mathrm{Type},\\ (\mathrm{Fintype}(Sample)\wedge \mathrm{Fintype}(Hidden)\wedge \forall i:Index,\mathrm{Fintype}(Output(i)))\Rightarrow \\ \forall mass:Sample\to \mathbb{R},hidden:Sample\to Hidden,\\ output:\forall i:Index,Sample\to Output(i),\\ S:\mathrm{Finset}(Index),T:\mathrm{Finset}(Index),\\ ((\forall s:Sample,0\le mass(s))\wedge \sum _{s:Sample}mass(s)=1)\wedge S\subseteq T\Rightarrow \\ \mathrm{mutualInformation}(\mathrm{readoutTargetLaw}(mass,\mathrm{jointReadout}(j:S\mapsto output(\mathrm{val}(j))),hidden))\le \mathrm{mutualInformation}(\mathrm{readoutTargetLaw}(mass,\mathrm{jointReadout}(j:T\mapsto output(\mathrm{val}(j))),hidden)).\end{array}$$

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

Source. Repository-derived.

Commentary.

Let the experiment index, hidden state, sample space, and each experiment-output alphabet be finite. A probability mass on samples and the hidden and experiment readouts construct each selected tuple through the canonical joint readout.

When S is contained in T, restricting a T-output tuple to S is deterministic postprocessing, so finite data processing gives the displayed inequality. Conditional independence is not needed for this monotonicity clause.

References

• Truth anchor: D5/S3/Entropy/Submodularity/SelectedObservationInformationMonotonicityCanonical.selected_observation_information_monotone_canonical
• Dependency: D5/S3/ConceptDynamics/Faithfulness/JointFaithfulnessLeibnizCriterion
• Dependency: D5/S3/Entropy/Submodularity/SelectedObservationInformationMonotonicity