Partition-Decision Adjunction

@cite{blackwell-1953} @cite{merin-1999} @cite{van-rooy-2003}

Galois connection between QUD partitions and decision problems, formalizing the Blackwell/Van Rooy correspondence.

Sufficient Partition

Given a decision problem dp with actions actions, the sufficient partition groups worlds by their utility vectors: w ~ v iff ∀ a ∈ actions, U(w,a) = U(v,a). This is the coarsest partition that preserves all utility-relevant distinctions.

Forward Galois Direction

If Q refines sufficientPartition dp actions, then within each Q-cell, all worlds have identical utility vectors. Any action that weakly dominates in one world of the cell dominates in all. Hence Q resolves dp.

Backward Direction (False)

The converse fails: Q may resolve dp without refining the sufficient partition. Example: U(w₁, a) = 1, U(w₁, b) = 0; U(w₂, a) = 3, U(w₂, b) = 0. Then w₁ and w₂ have different utility vectors (sufficient partition separates them), but Q = trivial resolves dp because action a globally dominates.

The sufficient partition is the coarsest partition preserving utility structure, not the coarsest partition resolving a particular dp.

Categorical Connection

The refinement morphism QUDHom Q (sufficientPartition dp actions) in PartitionCat witnesses the forward direction. Terminal morphisms (QUDHom.toTrivial) recover the fact that the trivial partition resolves only trivially dominable DPs.

def Theories.DTS.PartitionAdjunction.utilityEquiv {W : Type u_1} {A : Type u_2} (dp : Core.DecisionTheory.DecisionProblem W A) (actions : List A) (w v : W) : Bool

Two worlds are utility-equivalent for a decision problem and action list iff they yield identical utilities for every action.

Equations

• Theories.DTS.PartitionAdjunction.utilityEquiv dp actions w v = actions.all fun (a : A) => dp.utility w a == dp.utility v a

def Theories.DTS.PartitionAdjunction.sufficientPartition {W : Type u_1} {A : Type u_2} (dp : Core.DecisionTheory.DecisionProblem W A) (actions : List A) : QUD W

The sufficient partition for a decision problem: the coarsest partition that preserves all utility-relevant distinctions.

Two worlds are in the same cell iff they have identical utility vectors across all actions.

Equations

• Theories.DTS.PartitionAdjunction.sufficientPartition dp actions = { sameAnswer := Theories.DTS.PartitionAdjunction.utilityEquiv dp actions, refl := ⋯, symm := ⋯, trans := ⋯ }

theorem Theories.DTS.PartitionAdjunction.sufficientPartition_utility_eq {W : Type u_1} {A : Type u_2} (dp : Core.DecisionTheory.DecisionProblem W A) (actions : List A) {w v : W} (h : (sufficientPartition dp actions).sameAnswer w v = true) {a : A} (ha : a ∈ actions) : dp.utility w a = dp.utility v a

Within a sufficient partition cell, utilities are identical for every action.

theorem Theories.DTS.PartitionAdjunction.refinement_preserves_utility {W : Type u_1} {A : Type u_2} (dp : Core.DecisionTheory.DecisionProblem W A) (actions : List A) (q : QUD W) (hRef : q.refines (sufficientPartition dp actions)) {w v : W} (hCell : q.sameAnswer w v = true) {a : A} (ha : a ∈ actions) : dp.utility w a = dp.utility v a

If Q refines the sufficient partition, then within each Q-cell, all worlds have identical utilities for every listed action.

This is the key lemma: refinement → utility preservation.

theorem Theories.DTS.PartitionAdjunction.dominance_transfers_within_cell {W : Type u_1} {A : Type u_2} (dp : Core.DecisionTheory.DecisionProblem W A) (actions : List A) {w v : W} (hCell : (sufficientPartition dp actions).sameAnswer w v = true) {a : A} (ha : a ∈ actions) (hDom : ∀ b ∈ actions, dp.utility w a ≥ dp.utility w b) (b : A) : b ∈ actions → dp.utility v a ≥ dp.utility v b

Within a sufficient-partition cell, if any action weakly dominates all others at one world, it dominates at every world in the cell.

Dominance transfers because all worlds in the cell have identical utility vectors.

theorem Theories.DTS.PartitionAdjunction.sufficientPartition_cell_dominated {W : Type u_1} {A : Type u_2} (dp : Core.DecisionTheory.DecisionProblem W A) (actions : List A) {w v : W} (hCell : (sufficientPartition dp actions).sameAnswer w v = true) {a : A} (ha : a ∈ actions) (hBest : ∀ b ∈ actions, dp.utility w a ≥ dp.utility w b) : dp.utility v a ≥ dp.utility v (actions.head ⋯)

Within any cell of the sufficient partition, all worlds have the same utility vector, so the action with maximum utility (if it exists) weakly dominates all others throughout the cell.

This states that the sufficient partition resolves dp in the strong sense: for each cell, there exists a dominating action.

theorem Theories.DTS.PartitionAdjunction.sufficientPartition_coarsest {W : Type u_1} {A : Type u_2} (dp : Core.DecisionTheory.DecisionProblem W A) (actions : List A) (q : QUD W) (hUtil : ∀ (w v : W), q.sameAnswer w v = true → ∀ a ∈ actions, dp.utility w a = dp.utility v a) : q.refines (sufficientPartition dp actions)

The sufficient partition is the coarsest partition with utility-constant cells.

Any partition Q whose cells have identical utility vectors (i.e., Q refines utility equivalence) must refine the sufficient partition. This is immediate from the definitions.

def Theories.DTS.PartitionAdjunction.refinementMorphism {W : Type u_1} {A : Type u_2} (dp : Core.DecisionTheory.DecisionProblem W A) (actions : List A) (q : QUD W) (hRef : q.refines (sufficientPartition dp actions)) : Core.Categorical.QUDHom { qud := q } { qud := sufficientPartition dp actions }

A refinement morphism from Q to the sufficient partition, in the partition category. Witnesses the forward Galois direction categorically.

Equations

• Theories.DTS.PartitionAdjunction.refinementMorphism dp actions q hRef = { down := hRef }

theorem Theories.DTS.PartitionAdjunction.sufficient_trivial_of_constant_utility {W : Type u_1} {A : Type u_2} (dp : Core.DecisionTheory.DecisionProblem W A) (actions : List A) (hConst : ∀ (w v : W), ∀ a ∈ actions, dp.utility w a = dp.utility v a) : QUD.trivial.refines (sufficientPartition dp actions)

When all worlds have identical utility vectors (not just a dominant action), the sufficient partition is trivial. This is the case where world-state information has zero value for the decision problem.

The backward Galois direction is false

The converse of the forward direction — "Q resolves dp → Q refines sufficientPartition dp" — fails. A partition may resolve a decision problem by accident (a globally dominant action) without preserving utility-vector distinctions.

Counterexample: W = {w₁, w₂}, actions = {a, b}. U(w₁, a) = 1, U(w₁, b) = 0; U(w₂, a) = 3, U(w₂, b) = 0.

The sufficient partition separates w₁ and w₂ (utility vectors differ: [1, 0] vs [3, 0]). But Q = trivial resolves dp: action a dominates globally (U(w, a) > U(w, b) for all w). Yet trivial does NOT refine the sufficient partition.

This is expected: the sufficient partition preserves all utility information, while resolution only requires some action to dominate. The Galois connection is one-sided.

instance Theories.DTS.PartitionAdjunction.instDecidableEqGW : DecidableEq Theories.DTS.PartitionAdjunction.GW✝

Equations

• One or more equations did not get rendered due to their size.

instance Theories.DTS.PartitionAdjunction.instDecidableEqGA : DecidableEq Theories.DTS.PartitionAdjunction.GA✝

Equations

• One or more equations did not get rendered due to their size.

theorem Theories.DTS.PartitionAdjunction.counterex_not_equiv : (sufficientPartition Theories.DTS.PartitionAdjunction.counterexDP✝ [Theories.DTS.PartitionAdjunction.GA.a✝, Theories.DTS.PartitionAdjunction.GA.b✝]).sameAnswer Theories.DTS.PartitionAdjunction.GW.w₁✝ Theories.DTS.PartitionAdjunction.GW.w₂✝ = false

w₁ and w₂ are NOT equivalent in the sufficient partition.

theorem Theories.DTS.PartitionAdjunction.counterex_trivial_identifies : QUD.trivial.sameAnswer Theories.DTS.PartitionAdjunction.GW.w₁✝ Theories.DTS.PartitionAdjunction.GW.w₂✝ = true

But trivial doesn't separate them.

theorem Theories.DTS.PartitionAdjunction.counterex_trivial_not_refines : ¬QUD.trivial.refines (sufficientPartition Theories.DTS.PartitionAdjunction.counterexDP✝ [Theories.DTS.PartitionAdjunction.GA.a✝, Theories.DTS.PartitionAdjunction.GA.b✝])

So trivial does NOT refine the sufficient partition.

def Theories.DTS.PartitionAdjunction.dpRefinement {W : Type u_1} {A : Type u_2} (dp₁ dp₂ : Core.DecisionTheory.DecisionProblem W A) (actions : List A) : Prop

The sufficient partition gives a QUD refinement ordering on decision problems: dp₁ is "harder" than dp₂ iff sufficientPartition(dp₁) refines sufficientPartition(dp₂).

By Blackwell's theorem (proved in GSVanRooyBridge.lean), this is equivalent to dp₁ being informationally more demanding: any partition that resolves dp₁ also resolves dp₂.

Equations

• One or more equations did not get rendered due to their size.

theorem Theories.DTS.PartitionAdjunction.dpRefinement_refl {W : Type u_1} {A : Type u_2} (dp : Core.DecisionTheory.DecisionProblem W A) (actions : List A) : dpRefinement dp dp actions

dpRefinement is reflexive.

theorem Theories.DTS.PartitionAdjunction.dpRefinement_trans {W : Type u_1} {A : Type u_2} {dp₁ dp₂ dp₃ : Core.DecisionTheory.DecisionProblem W A} {actions : List A} (h₁₂ : dpRefinement dp₁ dp₂ actions) (h₂₃ : dpRefinement dp₂ dp₃ actions) : dpRefinement dp₁ dp₃ actions

dpRefinement is transitive.

def Theories.DTS.PartitionAdjunction.dpRefinementMorphism {W : Type u_1} {A : Type u_2} {dp₁ dp₂ : Core.DecisionTheory.DecisionProblem W A} {actions : List A} (h : dpRefinement dp₁ dp₂ actions) : Core.Categorical.QUDHom { qud := sufficientPartition dp₁ actions } { qud := sufficientPartition dp₂ actions }

Categorically: dpRefinement gives a morphism in the partition category.

Equations

• Theories.DTS.PartitionAdjunction.dpRefinementMorphism h = { down := h }