Policy Capability Monotonicity

Abstract

Refining a readout enlarges its implementable policy set.

Theorem 1.1 (Policy capability is monotone under refinement).

$$\forall X,C,D,U:\mathrm{Type},q_C:X\to C,q_D:X\to D,\mathrm{Refines}\left(q_C,q_D\right)\Rightarrow \mathrm{policyCapability}\left(q_C,U\right)\subseteq \mathrm{policyCapability}\left(q_D,U\right).$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/PolicyCapabilityMonotonicity.policy_capability_monotone (✓ std3). ∎

Source. Repository-derived.

Commentary.

The policy-capability set of a readout consists of all state-level actions obtained by composing the readout with a decision rule.

A refinement factor recovers the coarse value from the fine value. Precomposing every coarse decision rule with that factor gives the stated inclusion of policy-capability sets.

References

• Truth anchor: D5/S3/ConceptDynamics/PolicyCapabilityMonotonicity.policy_capability_monotone
• Dependency: D5/S3/ConceptDynamics/ConceptJoinUniversal