Predictive-Law Sufficiency Implies Decision Sufficiency

Abstract

A predictive-law factor determines expected losses and their minimizing actions.

Theorem 1.1 (Predictive-law sufficiency implies decision sufficiency).

$$\begin{array}{c}\forall X,C,Y,A:\mathrm{Type},\\ K:X\to \mathrm{PMF}(Y),CReadout:X\to C,\\ \ell :A\to Y\to \mathbb{R},\\ \mathrm{MeasurableSpace}(Y)\wedge \mathrm{MeasurableSingletonClass}(Y),\\ \forall x:X,a:A,\mathrm{expectedLoss}(K,\ell )\left(x,a\right):={\int }_Y\ell \left(a,y\right)dK\left(x\right),\\ \forall x:X,\mathrm{optimalActions}(K,\ell )\left(x\right):={\mathrm{argmin}}_{a\in A}\mathrm{expectedLoss}(K,\ell )\left(x,a\right),\\ \mathrm{Refines}(K,CReadout)\Rightarrow \\ \mathrm{Refines}(\mathrm{expectedLoss}(K,\ell ),CReadout)\wedge \mathrm{Refines}(\mathrm{optimalActions}(K,\ell ),CReadout).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Decision/PredictionLawDecisionSufficiency.prediction_law_sufficiency_implies_decision_sufficiency (✓ std3). ∎

Source. Repository-derived.

Commentary.

Expected loss is the total Lean integral of each action loss against the predicted PMF; no integrability premise is required to construct it.

The optimal-action readout is the full set of actions minimizing that same expected-loss profile. Both constructions compose with the supplied prediction factor map.

References

• Truth anchor: D5/S3/ConceptDynamics/Decision/PredictionLawDecisionSufficiency.prediction_law_sufficiency_implies_decision_sufficiency
• Dependency: D5/S3/ConceptDynamics/ConceptJoinUniversal