Blackwell Order and External Cost

Abstract

Blackwell dominance orders decision information but imposes no order on an independently assigned nonnegative implementation cost.

Theorem 1.1 (Blackwell dominance can have higher cost).

$$\begin{gathered} \exists P,Q:\mathrm{Kernel}\left(Bool,Bool\right),cost:\mathrm{ExperimentCost}\left(Bool,Bool\right), \\ P\ne Q\wedge \mathrm{BlackwellDominates}\left(P,Q\right)\wedge cost\left(P\right)>cost\left(Q\right). \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/Estimation/ExperimentCost/BlackwellCostOrthogonality.exists_blackwell_dominance_with_higher_cost (✓ std3). ∎

Source. Repository-derived.

Commentary.

Implementation cost is a named function from experiment kernels to nonnegative reals, with no compatibility axiom connecting it to Blackwell dominance.

The Boolean identity experiment Blackwell-dominates the constant erasure experiment. They are distinct, and assigning costs one and zero respectively gives the strict higher-cost direction.

Theorem 1.2 (Blackwell dominance can have lower cost).

$$\begin{gathered} \exists P,Q:\mathrm{Kernel}\left(Bool,Bool\right),cost:\mathrm{ExperimentCost}\left(Bool,Bool\right), \\ P\ne Q\wedge \mathrm{BlackwellDominates}\left(P,Q\right)\wedge cost\left(P\right)<cost\left(Q\right). \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/Estimation/ExperimentCost/BlackwellCostOrthogonality.exists_blackwell_dominance_with_lower_cost (✓ std3). ∎

Source. Repository-derived.

Commentary.

For the same distinct Boolean experiment pair, reversing the two assigned costs makes the dominating experiment strictly cheaper.

Together with the higher-cost witness, this shows that Blackwell dominance alone determines neither strict cost direction.

Theorem 1.3 (Equal experiments have equal cost).

$$\begin{gathered} \forall \theta ,X,cost:\mathrm{ExperimentCost}\left(\theta ,X\right), \\ P,Q:\mathrm{Kernel}\left(\theta ,X\right),P=Q\Rightarrow cost\left(P\right)=cost\left(Q\right). \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/Estimation/ExperimentCost/BlackwellCostOrthogonality.equal_experiments_have_equal_cost (✓ std3). ∎

Source. Repository-derived.

Commentary.

Because an external cost assignment is still a function, equal kernels must receive equal values by congruence.

Thus reflexive Blackwell dominance is not itself a strict-cost witness; the two existence theorems deliberately use distinct identity and erasure kernels.

Theorem 1.4 (Constant cost cannot strictly compare experiments).

$$\begin{gathered} \forall \theta ,X,c:{\mathbb{R}}_{\ge 0},P,Q:\mathrm{Kernel}\left(\theta ,X\right), \\ \neg \mathrm{constCost}\left(c\right)\left(P\right)>\mathrm{constCost}\left(c\right)\left(Q\right)\wedge \neg \mathrm{constCost}\left(c\right)\left(P\right)<\mathrm{constCost}\left(c\right)\left(Q\right). \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/Estimation/ExperimentCost/BlackwellCostOrthogonality.constant_experiment_cost_cannot_strictly_compare (✓ std3). ∎

Source. Repository-derived.

Commentary.

A constant assignment gives the same nonnegative value to every kernel, so neither strict comparison can hold for any pair.

Accordingly the concrete existence witnesses use nonconstant cost functions; their strict inequalities carry that requirement.

Theorem 1.5 (Constant Boolean experiments are Blackwell-equivalent).

$$\mathrm{BlackwellDominates}\left(K_0,K_1\right)\wedge \mathrm{BlackwellDominates}\left(K_1,K_0\right).$$

Proof. Machine-checked in Lean as D5/S3/Estimation/ExperimentCost/BlackwellCostOrthogonality.constant_boolean_experiments_are_blackwell_equivalent (✓ std3). ∎

Source. Repository-derived.

Commentary.

The always-false and always-true Boolean experiments can each be obtained from the other by constant deterministic processing.

This verifies the fully uninformative degenerate case directly and shows that mutual dominance supplies no external cost order.

Theorem 1.6 (Blackwell dominance still compares Bayes risk).

$$\begin{array}{c}\forall P:\mathrm{Kernel}\left(\theta ,X\right),Q:\mathrm{Kernel}\left(\theta ,X_1\right),\\ \mathrm{BlackwellDominates}\left(P,Q\right)\Rightarrow \\ \forall \ell :\theta \to Y\to ENNReal,\pi :\mathrm{Measure}\left(\theta \right),\\ \mathrm{bayesRisk}\left(\ell ,P,\pi \right)\le \mathrm{bayesRisk}\left(\ell ,Q,\pi \right).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Estimation/ExperimentCost/BlackwellCostOrthogonality.blackwell_dominance_still_compares_bayes_risk (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every extended-nonnegative loss and prior measure, a dominating experiment has no larger optimal Bayes risk.

This is a direct application of the established Blackwell theorem. Only the unrelated external cost comparison is unconstrained.

References

• Truth anchor: D5/S3/Estimation/ExperimentCost/BlackwellCostOrthogonality.blackwell_dominance_still_compares_bayes_risk
• Truth anchor: D5/S3/Estimation/ExperimentCost/BlackwellCostOrthogonality.constant_boolean_experiments_are_blackwell_equivalent
• Truth anchor: D5/S3/Estimation/ExperimentCost/BlackwellCostOrthogonality.constant_experiment_cost_cannot_strictly_compare
• Truth anchor: D5/S3/Estimation/ExperimentCost/BlackwellCostOrthogonality.equal_experiments_have_equal_cost
• Truth anchor: D5/S3/Estimation/ExperimentCost/BlackwellCostOrthogonality.exists_blackwell_dominance_with_higher_cost
• Truth anchor: D5/S3/Estimation/ExperimentCost/BlackwellCostOrthogonality.exists_blackwell_dominance_with_lower_cost
• Dependency: D5/S3/Estimation/DecisionRisk/GarblingIncreasesBayesRisk