Partition Lattice

@cite{blackwell-1953} @cite{groenendijk-stokhof-1984} @cite{merin-1999}

Refinement, coarsening, and cell enumeration for partitions (QUD).

Partitions arise wherever a domain is classified into mutually exclusive, exhaustive categories. @cite{groenendijk-stokhof-1984} use them for question denotations, but the lattice structure is domain-general: it applies equally to attribute spaces, conceptual categories, and any classificatory scheme.

Lattice Structure

Partitions form a bounded lattice ordered by refinement:

• Refinement (⊑): Q refines Q' iff Q's cells are subsets of Q''s
• Coarsening: dual — Q coarsens Q' iff Q' refines Q
• Meet (*): coarsest common refinement (QUD.compose)
• Top: exact partition (finest)
• Bottom: trivial partition (coarsest)

Decision-Theoretic Significance

@cite{merin-1999} argues that partitions are decision-theoretically privileged: coarsening preserves compositionality of expected value, while arbitrary restructuring does not. Negative attributes are products of proper coarsening — an epistemic, syntax-independent characterization of negativity.

Refinement and Coarsening

def QUD.refines {M : Type u_1} (q q' : QUD M) : Prop

Q refines Q' iff Q's equivalence classes are subsets of Q''s.

Intuitively: knowing the Q-answer tells you the Q'-answer. If two elements give the same Q-answer, they must give the same Q'-answer.

Forms a partial order on partitions (up to extensional equivalence).

Equations

• q.refines q' = ∀ (w v : M), q.sameAnswer w v = true → q'.sameAnswer w v = true

def QUD.«term_⊑_» : Lean.TrailingParserDescr

Equations

• QUD.«term_⊑_» = Lean.ParserDescr.trailingNode `QUD.«term_⊑_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊑ ") (Lean.ParserDescr.cat `term 51))

def QUD.coarsens {M : Type u_1} (q q' : QUD M) : Prop

Q coarsens Q' iff Q' refines Q (dual of refinement).

Coarsening merges cells: where Q' distinguishes elements, Q may not. @cite{merin-1999} defines negative attributes in terms of coarsening: negation is the linguistic device that produces coarsenings on the fly.

Equations

• q.coarsens q' = q'.refines q

theorem QUD.refines_refl {M : Type u_1} (q : QUD M) : q.refines q

Refinement is reflexive.

theorem QUD.refines_trans {M : Type u_1} {q1 q2 q3 : QUD M} : q1.refines q2 → q2.refines q3 → q1.refines q3

Refinement is transitive.

theorem QUD.refines_antisymm {M : Type u_1} {q1 q2 : QUD M} : q1.refines q2 → q2.refines q1 → ∀ (w v : M), q1.sameAnswer w v = q2.sameAnswer w v

Refinement is antisymmetric up to extensional equivalence of sameAnswer.

True propositional antisymmetry (q1 = q2) would require quotient types; this is the extensional version.

theorem QUD.all_refine_trivial {M : Type u_1} (q : QUD M) : q.refines trivial

All partitions refine (are coarser than or equal to) the trivial partition.

theorem QUD.compose_refines_left {M : Type u_1} (q1 q2 : QUD M) : (q1 * q2).refines q1

The meet (coarsest common refinement) refines the left factor.

theorem QUD.compose_refines_right {M : Type u_1} (q1 q2 : QUD M) : (q1 * q2).refines q2

The meet (coarsest common refinement) refines the right factor.

theorem QUD.exact_refines_all {M : Type u_1} [BEq M] [LawfulBEq M] (q : QUD M) : exact.refines q

The exact (finest) partition refines all partitions.

Finite Partition Cells

def QUD.toCells {M : Type u_1} (q : QUD M) (elements : List M) : List (M → Bool)

Compute partition cells as characteristic functions over a finite domain.

Each cell is the set of elements equivalent to a representative. Representatives are chosen greedily from the input list.

Equations

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

def QUD.numCells {M : Type u_1} (q : QUD M) (elements : List M) : ℕ

Number of cells in the partition over a finite domain.

Equations

• q.numCells elements = (q.toCells elements).length

Representative fold helpers

theorem QUD.refines_numCells_ge {M : Type u_1} (q q' : QUD M) (elements : List M) : q.refines q' → q.numCells elements ≥ q'.numCells elements

Finer partitions have at least as many cells.

The covering map from q'-representatives to q-representatives is injective (by pairwise inequivalence and refinement), giving |q-reps| ≥ |q'-reps|.

theorem QUD.toCells_sameAnswer_eq {M : Type u_1} (q : QUD M) (worlds : List M) (cell : M → Bool) (hcell : cell ∈ q.toCells worlds) (w v : M) (hsame : q.sameAnswer w v = true) : cell w = cell v

Cells of a QUD respect the equivalence relation: equivalent worlds agree on cell membership. If q.sameAnswer w v = true, then for any cell in q.toCells worlds, cell w = cell v.

theorem QUD.toCells_fine_sub_coarse {M : Type u_1} (q q' : QUD M) (worlds : List M) (hRefines : q.refines q') (c : M → Bool) (hc : c ∈ q.toCells worlds) : ∃ c' ∈ q'.toCells worlds, ∀ (w : M), c w = true → c' w = true

Each fine cell is contained in some coarse cell (w.r.t. toCells).

If q refines q' (q ⊑ q', finer partition), then for every fine cell c of q, there exists a coarse cell of q' containing it.

theorem QUD.toCells_coarse_contains_fine {M : Type u_1} (q q' : QUD M) (worlds : List M) (hRefines : q'.refines q) (c : M → Bool) (hc : c ∈ q.toCells worlds) : ∃ c' ∈ q'.toCells worlds, ∀ (w : M), c' w = true → c w = true

Each coarse cell contains some fine cell (w.r.t. toCells).

If q' refines q (q' ⊑ q, finer partition), then for every coarse cell c of q, there exists a fine cell of q' contained in it.

theorem QUD.toCells_cell_nonempty {M : Type u_1} (q : QUD M) (elements : List M) (c : M → Bool) (hc : c ∈ q.toCells elements) : ∃ w ∈ elements, c w = true

Each cell of toCells is nonempty: there exists an element in elements that belongs to the cell (namely, the cell's representative).

theorem QUD.toCells_nonempty {M : Type u_1} (q : QUD M) (w : M) (ws : List M) : q.toCells (w :: ws) ≠ []

toCells of a nonempty list is nonempty. Every element gets covered by a representative, so at least one representative (and cell) exists.

Proper Coarsening

def QUD.isProperCoarsening {M : Type u_1} (q q' : QUD M) (elements : List M) : Prop

Q is a proper coarsening of Q' over a finite domain iff Q coarsens Q' and has strictly fewer cells.

@cite{merin-1999} defines negative attributes via proper coarsening: R is a negative attribute with respect to partition F iff for some Q ∈ F, {R, Q} is a proper coarsening of F. This characterization is purely epistemic and syntax-independent — negativity is a matter of partition kinetics, not morphological form.

Equations

• q.isProperCoarsening q' elements = (q.coarsens q' ∧ q.numCells elements < q'.numCells elements)

Binary Partitions

@[reducible, inline]

abbrev QUD.binaryPartition {M : Type u_1} (p : M → Bool) : QUD M

Binary partition from a Boolean predicate. Two elements are equivalent iff the predicate gives the same value on both.

Binary partitions are the building blocks of coarsening: every proper coarsening can be decomposed into steps that merge exactly two cells, each corresponding to a binary partition. @cite{merin-1999} characterizes negative attributes entirely in terms of binary partition coarsening.

Equations

• QUD.binaryPartition p = QUD.ofProject p

theorem QUD.complement_same_partition {M : Type u_1} (p : M → Bool) (w v : M) : (binaryPartition p).sameAnswer w v = (binaryPartition fun (m : M) => !p m).sameAnswer w v

Complement predicates induce the same binary partition.

@cite{merin-1999}: a proposition and its negation carry exactly the same information. {P-worlds, ¬P-worlds} = {¬P-worlds, P-worlds} as partitions.

theorem QUD.binaryPartition_coarsens {M : Type u_1} (q : QUD M) (p : M → Bool) (h : ∀ (w v : M), q.sameAnswer w v = true → p w = p v) : (binaryPartition p).coarsens q

A binary partition from a predicate that respects q's equivalence classes is a coarsening of q. Every "coarser" yes/no distinction is a coarsening.

def QUD.isNegativeAttribute {M : Type u_1} (R : M → Bool) (q : QUD M) (elements : List M) : Prop

A predicate R is a negative attribute with respect to partition Q over a finite domain iff the binary partition of R is a proper coarsening of Q.

@cite{merin-1999}: negativity is not a syntactic property (presence of "un-", "not", etc.) but a partition-kinetic one. R is negative relative to Q when the R/¬R distinction is strictly coarser than Q's partition — answering whether R holds loses information that Q distinguishes.

Equations

• QUD.isNegativeAttribute R q elements = (QUD.binaryPartition R).isProperCoarsening q elements

Coarsest P-Preserving Coarsening (@cite{merin-1999}, Fact 3)

def QUD.coarsestPreserving {M : Type u_1} (q : QUD M) (P : M → Bool) : QUD M

The coarsest coarsening of Q that preserves predicate P.

Two elements are equivalent iff they are Q-equivalent AND agree on P. This is the meet of Q with the binary partition of P: the finest partition that is coarser than both Q and binaryPartition P.

@cite{merin-1999}: for any proposition P and partition Q, this is the unique coarsest partition that refines Q while still distinguishing P-worlds from ¬P-worlds within each Q-cell.

Equations

• q.coarsestPreserving P = q * QUD.binaryPartition P

theorem QUD.coarsestPreserving_refines {M : Type u_1} (q : QUD M) (P : M → Bool) : (q.coarsestPreserving P).refines q

The P-preserving coarsening refines Q (it can only be finer).

theorem QUD.coarsestPreserving_preserves_P {M : Type u_1} (q : QUD M) (P : M → Bool) (w v : M) (h : (q.coarsestPreserving P).sameAnswer w v = true) : P w = P v

The P-preserving coarsening respects P: equivalent elements agree on P.

theorem QUD.coarsestPreserving_universal {M : Type u_1} (q q' : QUD M) (P : M → Bool) (hrefines : q'.refines q) (hpreserves : ∀ (w v : M), q'.sameAnswer w v = true → P w = P v) : q'.refines (q.coarsestPreserving P)

Any partition that refines Q and preserves P also refines the P-preserving coarsening. This is the universality property: coarsestPreserving is the coarsest such partition.

Finpartition from QUD

def QUD.toFinpartition {M : Type u_1} [Fintype M] [DecidableEq M] (q : QUD M) : Finpartition Finset.univ

The Finpartition induced by a QUD over a Fintype.

Uses Mathlib's Finpartition.ofSetoid — exhaustivity, disjointness, and non-emptiness of cells come for free from the Finpartition structure.

Equations

• q.toFinpartition = Finpartition.ofSetoid q.toSetoid

EU Compositionality under Coarsening (@cite{merin-1999}, Central Theorem)

def QUD.partitionEU {M : Type u_1} [Fintype M] [DecidableEq M] {A : Type u_2} (dp : Core.DecisionTheory.DecisionProblem M A) (q : QUD M) (a : A) : ℚ

Expected utility computed via a partition: weight each cell's conditional EU by the cell's probability.

EU_Q(a) = Σ_{c ∈ cells(Q)} P(c) · EU(a | c)

This is the partition-relative expected utility that @cite{merin-1999} shows is compositional under coarsening. Uses Finpartition for exhaustivity and disjointness, replacing ~200 lines of custom foldl arithmetic.

Equations

• QUD.partitionEU dp q a = ∑ cell ∈ q.toFinpartition.parts, cell.sum dp.prior * Core.DecisionTheory.conditionalEU dp cell a

Cell probability cancellation (Finset version)

theorem QUD.eu_eq_partitionEU {M : Type u_1} [Fintype M] [DecidableEq M] {A : Type u_2} (dp : Core.DecisionTheory.DecisionProblem M A) (a : A) (q : QUD M) (hprior : ∀ (w : M), dp.prior w ≥ 0) : Core.DecisionTheory.expectedUtility dp a = partitionEU dp q a

Law of total expectation for partition-relative EU.

The unconditional expected utility equals the partition-relative EU for any partition, because partitions are exhaustive and mutually exclusive.

Uses Finset.sum_biUnion with Finpartition.biUnion_parts for the decomposition — disjointness and exhaustivity come free from the Finpartition structure.

Non-negativity is necessary: with prior(w1) = 1, prior(w2) = -1, utility(w1,a) = 1, utility(w2,a) = 0, and a trivial partition, expectedUtility = 1 but cellProb = 0 forces partitionEU = 0.

theorem QUD.coarsening_preserves_eu {M : Type u_1} [Fintype M] [DecidableEq M] {A : Type u_2} (dp : Core.DecisionTheory.DecisionProblem M A) (q q' : QUD M) (a : A) (_hcoarse : q.coarsens q') (hprior : ∀ (w : M), dp.prior w ≥ 0) : partitionEU dp q a = partitionEU dp q' a

Partition-relative EU is partition-independent (given non-negative priors).

Any two partitions give the same partition-relative EU, because both equal the unconditional EU (eu_eq_partitionEU).

Blackwell Ordering

Finset-based partition cells

def QUD.toCellsFinset {M : Type u_1} [DecidableEq M] (q : QUD M) (worlds : Finset M) : Finset (Finset M)

Partition cells of worlds under QUD q, as a Finset of Finsets. Each cell is the set of elements in worlds that are q-equivalent to some w.

Equations

• q.toCellsFinset worlds = Finset.image (fun (w : M) => {v ∈ worlds | q.sameAnswer w v = true}) worlds

Finset-based partition value

def QUD.partitionValue {M : Type u_1} [DecidableEq M] {A : Type u_2} (dp : Core.DecisionTheory.DecisionProblem M A) (q : QUD M) (worlds : Finset M) (actions : Finset A) : ℚ

The value of a decision problem under partition Q over a Finset of worlds.

V_Q(D, W) = Σ_{c ∈ cells(Q,W)} max_a [Σ_{w∈c} p(w)·u(w,a)]

Following @cite{merin-1999}, this uses raw weighted sums directly rather than factoring through conditional EU. The equivalence P(c) · max_a condEU(a,c) = max_a [Σ_{w∈c} p(w)·u(w,a)] holds when priors are non-negative. The raw form makes Blackwell's theorem a direct application of sub-additivity.

Equations

• QUD.partitionValue dp q worlds actions = ∑ cell ∈ q.toCellsFinset worlds, if h : actions.Nonempty then actions.sup' h fun (a : A) => ∑ w ∈ cell, dp.prior w * dp.utility w a else 0

Sub-additivity of max

Blackwell refinement theorem

theorem QUD.blackwell_refinement_value {M : Type u_1} [DecidableEq M] {A : Type u_2} (dp : Core.DecisionTheory.DecisionProblem M A) (q q' : QUD M) (worlds : Finset M) (actions : Finset A) (hrefines : q.refines q') (_hprior : ∀ (w : M), dp.prior w ≥ 0) : partitionValue dp q worlds actions ≥ partitionValue dp q' worlds actions

Blackwell's theorem for partitions: finer partitions are always at least as valuable as coarser ones, for any decision problem.

V_Q(D) ≥ V_{Q'}(D) for all decision problems D, whenever Q ⊑ Q'.

Proof: Working directly with raw weighted sums Σ_{w∈c} p(w)·u(w,a):

1. Each coarse cell's sum decomposes into fine cells (Finset.sum_biUnion)
2. Sub-additivity of max: max_a(Σᵢ fᵢ(a)) ≤ Σᵢ max_a(fᵢ(a))
3. Regrouping: fine cells grouped by coarse cell = all fine cells

Resolution–Value Saturation

theorem QUD.resolution_value_eq_exact {M : Type u_1} [Fintype M] [DecidableEq M] {A : Type u_2} [DecidableEq A] (dp : Core.DecisionTheory.DecisionProblem M A) (q : QUD M) (actions : Finset A) (hResolves : ∀ cell ∈ q.toCellsFinset Finset.univ, ∃ a ∈ actions, ∀ b ∈ actions, ∀ w ∈ cell, dp.utility w a ≥ dp.utility w b) (hPrior : ∀ (w : M), dp.prior w ≥ 0) : partitionValue dp q Finset.univ actions = partitionValue dp exact Finset.univ actions

Resolution–Value Saturation: when every cell of partition Q has a dominant action, Q's partition value equals the exact partition's value.

This is the mathematical core of @cite{van-rooy-2003}: resolving partitions achieve the same value as the finest partition, so coarsening from G&S exhaustive answers to mention-some answers is decision-theoretically free.

Proof: Blackwell gives ≤ (exact refines all). For ≥, the dominant action achieves the pointwise maximum at every world in the cell, making the sub-additivity inequality tight.

Blackwell characterization

theorem QUD.blackwell_characterizes_refinement {M : Type u_1} [DecidableEq M] (q q' : QUD M) (h : ∀ (worlds : Finset M) (A : Type) [DecidableEq A] (dp : Core.DecisionTheory.DecisionProblem M A) (actions : Finset A), (∀ (w : M), dp.prior w ≥ 0) → partitionValue dp q worlds actions ≥ partitionValue dp q' worlds actions) : q.refines q'

Blackwell ordering characterizes refinement: Q refines Q' if and only if Q is at least as valuable as Q' for every decision problem.

This is the converse of blackwell_refinement_value: if Q is always at least as valuable, then Q must refine Q'. Together they establish that partition refinement IS Blackwell ordering.

Proof (contrapositive): Suppose q does not refine q', i.e., ∃ w v with q.sameAnswer w v = true but q'.sameAnswer w v = false. Construct a DP over worlds = {w, v} with two actions where distinguishing w from v matters. Then q' achieves value 1 while q achieves 1/2.

Question Utility Bridge

Connect Finset-based questionUtility (from Core.DecisionTheory) to Finset-based partitionValue. The algebraic identity:

questionUtility dp actions (q.toCellsFinset Finset.univ) = partitionValue dp q Finset.univ actions - dpValue dp actions * (Finset.univ : Finset M).sum dp.prior

under non-negative priors. Since dpValue * totalPrior is partition-independent, the Blackwell ordering on partitionValue transfers directly to questionUtility.

Per-cell equivalence

Cells partition Finset.univ

Main bridge theorem

theorem QUD.questionUtility_refinement_ge {M : Type u_2} [Fintype M] [DecidableEq M] {A : Type u_3} [DecidableEq A] (dp : Core.DecisionTheory.DecisionProblem M A) (q q' : QUD M) (actions : Finset A) (hRefines : q.refines q') (hprior : ∀ (w : M), dp.prior w ≥ 0) : Core.DecisionTheory.questionUtility dp actions (q.toCellsFinset Finset.univ) ≥ Core.DecisionTheory.questionUtility dp actions (q'.toCellsFinset Finset.univ)

Blackwell ordering on questionUtility for QUD-derived questions.

Refinement implies higher question utility (with non-negative priors).

Proof: questionUtility = partitionValue - dpValue × totalPrior. Since dpValue and totalPrior are partition-independent, the ordering on partitionValue (from blackwell_refinement_value) transfers.

theorem QUD.partitionValue_ge_of_questionUtility_ge {M : Type u_2} [Fintype M] [DecidableEq M] {A : Type u_3} [DecidableEq A] (dp : Core.DecisionTheory.DecisionProblem M A) (q q' : QUD M) (actions : Finset A) (hprior : ∀ (w : M), dp.prior w ≥ 0) (hQU : Core.DecisionTheory.questionUtility dp actions (q.toCellsFinset Finset.univ) ≥ Core.DecisionTheory.questionUtility dp actions (q'.toCellsFinset Finset.univ)) : partitionValue dp q Finset.univ actions ≥ partitionValue dp q' Finset.univ actions

questionUtility ordering implies partitionValue ordering on Finset.univ.

The identity questionUtility(q) = partitionValue(q, univ) - dpValue × totalPrior means the partition-independent constant cancels in comparisons.

Partition value restricted to prior support

When priors are zero outside a subset S, the partition value over the full universe equals the partition value over S. This bridges from questionUtility (which operates over Finset.univ) to partitionValue over arbitrary world sets (needed by blackwell_characterizes_refinement).

theorem QUD.partitionValue_restrict_support {M : Type u_2} [Fintype M] [DecidableEq M] {A : Type u_3} (dp : Core.DecisionTheory.DecisionProblem M A) (q : QUD M) (S : Finset M) (actions : Finset A) (hsupp : ∀ w ∉ S, dp.prior w = 0) : partitionValue dp q Finset.univ actions = partitionValue dp q S actions

Partition value restricted to prior support.

When priors are zero outside S, partitionValue over Finset.univ equals partitionValue over S. Cells not intersecting S contribute zero (all priors are 0). Cells intersecting S have the same per-cell value as the S-restricted cells. The bijection between nonempty-in-S cells and toCellsFinset S reindexes the sum.

theorem QUD.partitionValue_congr_on_worlds {M : Type u_2} [DecidableEq M] {A : Type u_3} (dp dp' : Core.DecisionTheory.DecisionProblem M A) (q : QUD M) (worlds : Finset M) (actions : Finset A) (h : ∀ w ∈ worlds, dp.prior w = dp'.prior w ∧ ∀ (a : A), dp.utility w a = dp'.utility w a) : partitionValue dp q worlds actions = partitionValue dp' q worlds actions

partitionValue depends only on dp.prior and dp.utility within worlds.

If two DPs agree on all worlds in worlds, they produce the same partition value, because each cell in toCellsFinset worlds is a subset of worlds.

QUD question utility non-negativity

theorem QUD.questionUtility_qud_nonneg {M : Type u_2} [Fintype M] [DecidableEq M] {A : Type u_3} [DecidableEq A] (dp : Core.DecisionTheory.DecisionProblem M A) (q : QUD M) (actions : Finset A) (hprior : ∀ (w : M), dp.prior w ≥ 0) (hsum : Finset.univ.sum dp.prior = 1) : Core.DecisionTheory.questionUtility dp actions (q.toCellsFinset Finset.univ) ≥ 0

QUD-derived questionUtility is non-negative under proper priors.

Requires non-negative priors summing to exactly 1 (proper probability).

Proof: questionUtility(q) ≥ questionUtility(trivial) by Blackwell (questionUtility_refinement_ge + all_refine_trivial). Then questionUtility(trivial) = 0 because conditioning on the full universe with totalProb = 1 yields conditionalEU = expectedUtility, so valueAfterLearning = dpValue and utilityValue = 0.