Information Value Monotonicity

Abstract

Free ignorable refinement with unchanged actions cannot lower optimal value.

Theorem 1.1 (Free information refinement cannot lower optimal value).

$$\begin{array}{c}\forall X,C,D,U:\mathrm{Type},\\ \mathbb{E}:\mathrm{Concept}\left(X\to \mathbb{R},\mathbb{R}\right),q_C:\mathrm{Concept}\left(X,C\right),\\ q_D:\mathrm{Concept}\left(X,D\right),T:D\to X\to X,\\ V:\mathrm{Concept}\left(X,U\to \mathbb{R}\right),c:\mathbb{R},\\ U_C:C\to \mathrm{Set}\left(U\right),U_D:D\to \mathrm{Set}\left(U\right),\\ {\pi }_C:\mathrm{Set}\left(C\to U\right),{\pi }_D:\mathrm{Set}\left(D\to U\right),\\ W_C,W_D:\mathbb{R},\\ c=0,\\ \forall d:D,x:X,T(d)(x)=x,\\ \exists p:D\to C,q_C=p\circ q_D\wedge \\ (\forall d:D,U_D(d)=U_C(p(d)))\wedge \\ (\forall p_C:C\to U,p_C\in {\pi }_C\Rightarrow p_C\circ p\in {\pi }_D),\\ W_C=\underset{p_C\in \mathrm{admissiblePolicies}\left({\pi }_C,U_C\right)}{\max }\mathrm{informedExpectedValue}\left(\mathbb{E},q_C,\mathrm{idWorld},V,0,p_C\right),\\ W_D=\underset{p_D\in \mathrm{admissiblePolicies}\left({\pi }_D,U_D\right)}{\max }\mathrm{informedExpectedValue}\left(\mathbb{E},q_D,T,V,c,p_D\right)\\ \Rightarrow W_D\ge W_C.\end{array}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/DecisionValue/InformationValueMonotonicity.free_information_refinement_value_monotone (✓ std3). ∎

Source. Repository-derived.

Commentary.

The coarse and fine policy values use the same expectation and utility. The fine value additionally evaluates the post-information world and subtracts the information cost.

The public factor witness states concept refinement. Its remaining public clauses say that action sets are exactly preserved through the factor and every coarse candidate policy can ignore the added information by composition.

Lift a policy attaining the coarse optimum along the forgetting map. Exact action preservation makes it admissible; zero cost and the unchanged world make its fine value equal to the coarse optimum. Fine optimality then supplies the comparison.

References

• Truth anchor: D5/S3/ConceptDynamics/DecisionValue/InformationValueMonotonicity.free_information_refinement_value_monotone
• Dependency: D5/S3/ConceptDynamics/DecisionValue/FreeInformationValue