Partition Cells

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

Concrete cell enumeration for partitions (QUD) over finite domains:

• toCells / numCells — List-based cells via greedy representative fold.
• toFinpartition — bridge to mathlib's Finpartition (exhaustivity and disjointness for free).
• toCellsFinset and helpers — Finset-based cells used by the decision- theoretic bridge in Core/Agent/PartitionDT.lean.

The two views are complementary: toCells gives a chosen ordering of representatives (useful for induction), while toCellsFinset is unordered and plays nicely with Finset.sum_biUnion decompositions.

Cell-membership operator (G&S Ch I)

ans Q i returns the characteristic function of the cell of Q's partition containing i — (@cite{groenendijk-stokhof-1984}, p. 14-15). This is substrate; paper-specific theorems about answerhood (Karttunen completeness, Belnap distributivity, mention-some, exhaustivity ladder) live in the topical files under Theories/Semantics/Questions/.

def QUD.ans {M : Type u_1} (q : QUD M) (i : M) : M → Bool

ans Q i = the cell of Q's partition containing i.

Equations

• q.ans i w = q.sameAnswer i w

theorem QUD.ans_true_at_index {M : Type u_1} (q : QUD M) (i : M) : q.ans i i = true

ans is true at the index of evaluation.

theorem QUD.ans_constant_on_cells {M : Type u_1} (q : QUD M) (w v : M) (hEquiv : q.r w v) (u : M) : q.ans w u = q.ans v u

Worlds in the same cell get the same ans extension.

theorem QUD.ans_disjoint {M : Type u_1} (q : QUD M) (w v u : M) (hNotEquiv : ¬q.r w v) : ¬(q.ans w u = true ∧ q.ans v u = true)

ans propositions from different cells are disjoint.

Finite Partition Cells

def QUD.toCells {M : Type u_1} [DecidableEq M] (q : QUD M) (elements : List M) : List (Finset M)

Compute partition cells as Finsets over a finite domain.

Each cell is the set of elements equivalent to a representative, restricted to the input list. 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} [DecidableEq M] (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} [DecidableEq M] (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} [DecidableEq M] (q : QUD M) (worlds : List M) (cell : Finset M) (hcell : cell ∈ q.toCells worlds) (w v : M) (hwmem : w ∈ worlds) (hvmem : v ∈ worlds) (hsame : q.sameAnswer w v = true) : w ∈ cell ↔ v ∈ cell

Cells of a QUD respect the equivalence relation: for any cell in q.toCells worlds, if q.sameAnswer w v = true and both w, v ∈ worlds, then w ∈ cell ↔ v ∈ cell.

theorem QUD.toCells_fine_sub_coarse {M : Type u_1} [DecidableEq M] (q q' : QUD M) (worlds : List M) (hRefines : q.refines q') (c : Finset M) (hc : c ∈ q.toCells worlds) : ∃ c' ∈ q'.toCells worlds, c ⊆ c'

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} [DecidableEq M] (q q' : QUD M) (worlds : List M) (hRefines : q'.refines q) (c : Finset M) (hc : c ∈ q.toCells worlds) : ∃ c' ∈ q'.toCells worlds, c' ⊆ c

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} [DecidableEq M] (q : QUD M) (elements : List M) (c : Finset M) (hc : c ∈ q.toCells elements) : ∃ w ∈ elements, w ∈ c

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} [DecidableEq M] (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.

theorem QUD.toCells_covers {M : Type u_1} [DecidableEq M] (q : QUD M) (elements : List M) (w : M) (hw : w ∈ elements) : ∃ c ∈ q.toCells elements, w ∈ c

Every element in the input list belongs to some cell of toCells.

theorem QUD.toCells_exists_rep {M : Type u_1} [DecidableEq M] (q : QUD M) (elements : List M) (c : Finset M) (hc : c ∈ q.toCells elements) : ∃ rep ∈ elements, ∀ (w : M), w ∈ c ↔ w ∈ elements ∧ q.sameAnswer rep w = true

Every cell in toCells has a representative from the input list, and cell membership is w ∈ elements ∧ q.sameAnswer rep w.

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

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

theorem QUD.toCellsFinset_covers {M : Type u_1} [DecidableEq M] (q : QUD M) (worlds : Finset M) : (q.toCellsFinset worlds).biUnion id = worlds

Every world belongs to some cell in toCellsFinset.

theorem QUD.toCellsFinset_pairwiseDisjoint {M : Type u_1} [DecidableEq M] (q : QUD M) (worlds : Finset M) : (↑(q.toCellsFinset worlds)).PairwiseDisjoint id

Cells from toCellsFinset are pairwise disjoint.

theorem QUD.fine_cell_sub_coarse_finset {M : Type u_1} [DecidableEq M] (q q' : QUD M) (worlds : Finset M) (hrefines : q.refines q') (c : Finset M) (hc : c ∈ q.toCellsFinset worlds) : ∃ c' ∈ q'.toCellsFinset worlds, c ⊆ c'

Under refinement, each fine cell is a subset of some coarse cell.

theorem QUD.coarse_eq_biUnion_fine {M : Type u_1} [DecidableEq M] (q q' : QUD M) (worlds : Finset M) (hrefines : q.refines q') (c' : Finset M) (hc' : c' ∈ q'.toCellsFinset worlds) : c' = {x ∈ q.toCellsFinset worlds | x ⊆ c'}.biUnion id

A coarse cell equals the union of fine cells within it.

theorem QUD.fine_cells_in_coarse_pairwiseDisjoint {M : Type u_1} [DecidableEq M] (q : QUD M) (worlds c' : Finset M) : (↑({x ∈ q.toCellsFinset worlds | x ⊆ c'})).PairwiseDisjoint id

Fine cells within a coarse cell are pairwise disjoint (inherited from the fine partition being pairwise disjoint).