Causal Posterior Sufficiency

Abstract

A finite causal posterior determines future predictions and Bayes decisions.

Theorem 1.1 (The causal posterior determines prediction and decision).

$$\begin{array}{c}\forall M,H,I,Y:Type,\\ \mathrm{Fintype}(M),w:M\to H\to NNReal,\\ L:I\to M\to \mathrm{PMF}(Y),\\ h,h^{\prime }:H,\mathrm{posterior}(w,h)=\mathrm{posterior}(w,h^{\prime })\Rightarrow \\ (\forall i:I,y:Y,\mathrm{sum}(m,\mathrm{posterior}(w,h)(m)\times L(i)(m)(y))=\mathrm{sum}(m,\mathrm{posterior}(w,h^{\prime })(m)\times L(i)(m)(y)))\\ \wedge \\ (\forall i:I,A:Type,ell:M\to A\to ENNReal,\mathrm{setOf}(d,\forall d^{\prime }:Y\to A,\mathrm{sum}(m,\mathrm{posterior}(w,h)(m)\times \mathrm{tsum}(y,L(i)(m)(y)\times ell(m)(d(y))))\le \mathrm{sum}(m,\mathrm{posterior}(w,h)(m)\times \mathrm{tsum}(y,L(i)(m)(y)\times ell(m)(d^{\prime }(y)))))=\mathrm{setOf}(d,\forall d^{\prime }:Y\to A,\mathrm{sum}(m,\mathrm{posterior}(w,h^{\prime })(m)\times \mathrm{tsum}(y,L(i)(m)(y)\times ell(m)(d(y))))\le \mathrm{sum}(m,\mathrm{posterior}(w,h^{\prime })(m)\times \mathrm{tsum}(y,L(i)(m)(y)\times ell(m)(d^{\prime }(y)))))).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Estimation/DecisionRisk/CausalPosteriorSufficiency.causal_posterior_determines_predictions_and_bayes_decisions (✓ std3). ∎

Source. Repository-derived.

Commentary.

The model carrier is finite and histories induce the canonical normalized posterior from their joint weights. A future law is indexed only by the selected intervention and true model, so it contains no direct history argument.

The first displayed conclusion constructs every future-output predictive mass by mixing that model-conditioned law against the current posterior. Thus every intervention and output is covered publicly.

The second conclusion constructs posterior expected loss for every output-dependent decision rule and equates the full sets of minimizers. This states Bayes-decision sufficiency directly, rather than exposing only an optimal value.

References

• Truth anchor: D5/S3/Estimation/DecisionRisk/CausalPosteriorSufficiency.causal_posterior_determines_predictions_and_bayes_decisions
• Dependency: D5/S3/Estimation/DecisionRisk/PosteriorFuturePolicySufficiency