Prediction determines losses and actions, but actions need not determine prediction.
Theorem 1.1 (Prediction sufficiency implies decision sufficiency strictly).
∀ X ∈ T y p e , C ∈ T y p e , O u t co m e ∈ T y p e , A c t i o n ∈ T y p e , ( MeasurableSpace ( O u t co m e ) ∧ MeasurableSingletonClass ( O u t co m e ) ) ⇒ ( ∀ p re d i c t i o n ∈ X → PMF ( O u t co m e ) , co n ce pt ∈ X → C , l oss ∈ A c t i o n → ( O u t co m e → R ) , let e x p ec t e d L oss : X → ( A c t i o n → R ) , ∀ s t a t e ∈ X , a c t i o n ∈ A c t i o n , e x p ec t e d L oss ( s t a t e , a c t i o n ) = integral ( toMeasure ( p re d i c t i o n ( s t a t e ) ) , l oss ( a c t i o n ) ) ; let o pt ima l A c t i o n s : X → Set ( A c t i o n ) , ∀ s t a t e ∈ X , o pt ima l A c t i o n s ( s t a t e ) = { a c t i o n : A c t i o n ∣ ∀ a lt er na t i v e ∈ A c t i o n , e x p ec t e d L oss ( s t a t e , a c t i o n ) ≤ e x p ec t e d L oss ( s t a t e , a lt er na t i v e ) } ; ( Refines ( p re d i c t i o n , co n ce pt ) ⇒ ( Refines ( e x p ec t e d L oss , co n ce pt ) ∧ Refines ( o pt ima l A c t i o n s , co n ce pt ) ) ) ∧ let p re d i c t i o n E x am pl e : B oo l → PMF ( B oo l ) , ∀ s t a t e ∈ B oo l , p re d i c t i o n E x am pl e ( s t a t e ) = pure ( s t a t e ) ; let l oss E x am pl e : B oo l → ( B oo l → R ) , ∀ a c t i o n ∈ B oo l , o u t co m e ∈ B oo l , l oss E x am pl e ( a c t i o n , o u t co m e ) = if ( a c t i o n , 0 , if ( o u t co m e , 2 , 1 ) ) ; let e x p ec t e d L oss E x am pl e : B oo l → ( B oo l → R ) , ∀ s t a t e ∈ B oo l , a c t i o n ∈ B oo l , e x p ec t e d L oss E x am pl e ( s t a t e , a c t i o n ) = integral ( toMeasure ( p re d i c t i o n E x am pl e ( s t a t e ) ) , l oss E x am pl e ( a c t i o n ) ) ; let o pt ima l A c t i o n s E x am pl e : B oo l → Set ( B oo l ) , ∀ s t a t e ∈ B oo l , o pt ima l A c t i o n s E x am pl e ( s t a t e ) = { a c t i o n : B oo l ∣ ∀ a lt er na t i v e ∈ B oo l , e x p ec t e d L oss E x am pl e ( s t a t e , a c t i o n ) ≤ e x p ec t e d L oss E x am pl e ( s t a t e , a lt er na t i v e ) } ; let co n ce ptE x am pl e : B oo l → U ni t , ∀ s t a t e ∈ B oo l , co n ce ptE x am pl e ( s t a t e ) = u ni t ; Refines ( o pt ima l A c t i o n s E x am pl e , co n ce ptE x am pl e ) ∧ ¬ Refines ( p re d i c t i o n E x am pl e , co n ce ptE x am pl e ) )
Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Decision/PredictionDecisionSufficiencyStrictness.prediction_sufficiency_implies_decision_sufficiency_strictly✓ std3). ∎
Source. Repository-derived.
Commentary.
Factoring a predictive PMF through a concept factors both its complete expected-loss profile and the optimizer-set readout through that concept.
The converse countermodel uses two distinct deterministic predictive laws. Its outcome-dependent loss makes true the unique optimizer in both states, so one constant concept determines the actions but not the predictive law.