Strict Policy Power Growth

Abstract

Separating one coarse fiber with a finer readout strictly increases policy power.

Theorem 1.1 (A separated coarse fiber yields a genuinely new policy).

$$\forall X,C,D,U:\mathrm{Type},q_C:X\to C,q_D:X\to D,x,y:X,q_C(x)=q_C(y)\wedge q_D(x)\ne q_D(y)\wedge \exists u_0,u_1:U,u_0\ne u_1\Rightarrow \exists policy:X\to U,policy\in \mathrm{policyCapability}\left(q_D,U\right)\wedge \neg policy\in \mathrm{policyCapability}\left(q_C,U\right)\wedge policy(x)\ne policy(y)\wedge \forall coarsePolicy:X\to U,coarsePolicy\in \mathrm{policyCapability}\left(q_C,U\right)\Rightarrow coarsePolicy(x)=coarsePolicy(y).$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Policy/StrictPolicyPowerGrowth.strict_policy_power_growth (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let two states have the same coarse coordinate but distinct fine coordinates. Given two distinct actions, a decision rule on the fine coordinate can assign one action to the fine coordinate of the first state and the other action everywhere else. The induced state policy therefore distinguishes the two states.

Every policy available from the coarse readout factors through its coarse coordinate, so it must take equal values on those states. Consequently the separating policy belongs to the fine capability but not the coarse capability, while all coarse policies satisfy the universal non-separation conclusion.

The result needs neither surjectivity nor a global strict-refinement hypothesis: one explicitly separated pair inside a coarse fiber already witnesses strict local growth of policy power.

References

• Truth anchor: D5/S3/ConceptDynamics/Policy/StrictPolicyPowerGrowth.strict_policy_power_growth
• Dependency: D5/S3/ConceptDynamics/PolicyCapabilityMonotonicity