Target-Pair Coverage and Information Contrast

Abstract

Finite target identification is a pair-cover condition that positive statistical information alone need not satisfy.

Theorem 1.1 (Target-pair coverage is not replaced by mutual information).

$$\begin{array}{r}(\forall n:Nat,E,R,Y:\mathrm{Type},\\ \mathrm{DecidableEq}\left(E\right)\Rightarrow \forall A:\mathrm{Finset}\left(E\right),\\ r:E\to \mathrm{Fin}\left(n\right)\to R,T:\mathrm{Fin}\left(n\right)\to Y,\\ (\forall i,j:\mathrm{Fin}\left(n\right),T(i)\ne T(j)\Rightarrow \exists a\in A,\\ r(a)(i)\ne r(a)(j))⟺\\ \{\{i,j\}\mid T(i)\ne T(j)\}\subseteq \mathrm{Union}\left(a\in A,\{\{i,j\}\mid r(a)(i)\ne r(a)(j)\}\right))\wedge \\ (\mathrm{let}\mu :Bool\times Bool\to \mathbb{R}:=((b,c)\mapsto \mathrm{if}\left(b=false,\frac{1}{2},0\right)),\\ e:Bool\times Bool\to Bool:=((b,c)\mapsto c),\\ T:Bool\times Bool\to Bool:=((b,c)\mapsto b)\\ \mathrm{mutualInformation}\left(\mathrm{readoutTargetLaw}\left(\mu ,e,id\right)\right)=\log 2\wedge e((false,false))\ne e((false,true))\wedge \\ T((false,false))=T((false,true))\wedge e((false,false))=e((true,false))\wedge \\ T((false,false))\ne T((true,false))\wedge \neg \exists f:Bool\to Bool,T=f\circ e).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Experiment/TargetPairCoverageInformationContrast.target_pair_coverage_and_information_contrast (✓ std3). ∎

Source. Repository-derived.

Commentary.

For finitely indexed models and a finite selected experiment set, target identification is equivalent to covering every unordered target-disagreement pair by one selected experiment’s separation set. This is the finite hitting-set form of the cover criterion.

The concrete prior is supported on two models with the same target. Reading the nuisance coordinate carries exactly log two nats about the full model and separates those same-target models.

A second displayed pair has different targets but the same experiment response. Consequently the target cannot factor through the experiment, despite its positive model information.

References

• Truth anchor: D5/S3/ConceptDynamics/Experiment/TargetPairCoverageInformationContrast.target_pair_coverage_and_information_contrast
• Dependency: D5/S3/ConceptDynamics/Communication/TranslationLossMonotonicity
• Dependency: D5/S3/ConceptDynamics/Interventions/TargetRelativePairUniverse