Readout Refinement as Blackwell Garbling

Abstract

Measurable readout factorization becomes deterministic Blackwell garbling and Bayes-risk monotonicity.

Theorem 1.1 (Finer measurable readouts have no larger optimal Bayes risk).

$$\begin{array}{c}\forall q_C,q_D,L,mu:\mathrm{MeasurableRefines}(q_C,q_D)\Rightarrow \\ \mathrm{bayesRisk}(L,\mathrm{deterministic}(q_D),mu)\le \mathrm{bayesRisk}(L,\mathrm{deterministic}(q_C),mu).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/ReadoutBlackwellAdapter.bayesRisk_mono_of_measurable_refinement (✓ std3). ∎

Source. Repository-derived.

Commentary.

Measurable refinement augments the repository factorization preorder with the measurability required to form deterministic kernels.

Mathlib’s deterministic-kernel composition identity turns the factor map into a Blackwell garbling from the finer readout to the coarse readout.

The existing repository Blackwell theorem then gives Bayes-risk monotonicity for every prior, measurable decision space, and ENNReal-valued loss.

References

• Truth anchor: D5/S3/ConceptDynamics/ReadoutBlackwellAdapter.bayesRisk_mono_of_measurable_refinement
• Dependency: D5/S3/ConceptDynamics/ConceptJoinUniversal
• Dependency: D5/S3/Estimation/DecisionRisk/GarblingIncreasesBayesRisk