Support Gap Target Law

Abstract

A target branch outside behavior support admits data-equivalent transition models with different target laws.

Theorem 1.1 (Missing behavior support leaves the target law undetermined).

$$\begin{gathered} \mathrm{TargetBranchMass}(pi,h,a)\ne 0\wedge \mathrm{BehaviorMass}(mu,h,a)=0\wedge yZero\ne yOne\Rightarrow \\ \exists M,N, \\ \mathrm{Transition}(M,h,a)\ne \mathrm{Transition}(N,h,a)\wedge \\ (\forall hPrime,aPrime,\mathrm{BehaviorMass}(mu,hPrime,aPrime)\ne 0\Rightarrow \mathrm{Transition}(M,hPrime,aPrime)=\mathrm{Transition}(N,hPrime,aPrime))\wedge \\ \mathrm{TargetOutcomeLaw}(pi,M)\ne \mathrm{TargetOutcomeLaw}(pi,N). \end{gathered}$$

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

Source. Repository-derived.

Commentary.

The target branch law gives positive mass to the selected history-action pair, while the behavior policy assigns zero mass to its action at that history.

The first transition mechanism is constant. The second changes only the unsupported selected branch, so the two mechanisms agree at every branch carrying nonzero behavior mass.

Pushing the target branch law through the mechanisms yields different outcome laws: the positive selected atom reaches the distinct second outcome only under the second mechanism.

References

• Truth anchor: D5/S3/ConceptDynamics/Policy/SupportGapTargetLaw.support_gap_target_law