Core/Partition.lean dissolution: 4 per-purpose Question/Partition/ modules + DT extracted to Core/Agent/PartitionDT.lean (Direction A Setoid-canonical, 21 consumers); pre-existing Interval Time [LE Time]→[LinearOrder Time] cascade fixed across 13 downstream Ev/Eventuality/Interval consumer files (0.230.108)

Author: hawkrobe

CHANGELOG.md

@@ -4,6 +4,73 @@ The release clock (`v4.29.1`, ...) tracks Lean/mathlib compatibility and is what
 
 ## [Unreleased]
 
+## [0.230.108] - 2026-04-21
+
+### Changed
+- **`Core/Partition.lean` dissolved into `Core/Question/Partition/`** —
+  the 1360-line straggler is now four per-purpose modules sharing a
+  single Setoid-canonical foundation:
+  - `Core/Question/Partition/QUD.lean` (moved from
+    `Core/Question/QUD.lean`): `QUD M = {toSetoid : Setoid M, decR :
+    DecidableRel toSetoid.r}`. The bundled-Setoid struct preserves the
+    Bool API for ~335 consumer call sites while making the
+    Setoid-canonical structure explicit.
+  - `Core/Question/Partition/Basic.lean` (moved from
+    `Core/Question/Partition.lean`): `IsPartition` predicate (over
+    `Setoid.IsPartition`), `toSetoid`/`toQUD` bridges.
+  - `Core/Question/Partition/Lattice.lean` (new, ~89 LOC): refinement
+    order — `refines` (`⊑`), `coarsens`, reflexivity / transitivity /
+    antisymmetry, `all_refine_trivial`, `compose_refines_left`/right,
+    `exact_refines_all`.
+  - `Core/Question/Partition/Cells.lean` (new, 394 LOC): concrete
+    enumeration — `toCells`, `numCells`, `stepFn` and rep-fold helpers,
+    `toCells_*` theorems, `toFinpartition`, `toCellsFinset`,
+    coverage/disjointness lemmas, fine/coarse refinement lemmas.
+  - `Core/Question/Partition/Binary.lean` (new, 95 LOC): yes/no
+    partitions — `binaryPartition`, `complement_same_partition`,
+    `binaryPartition_coarsens`, `coarsestPreserving` and its
+    refinement/preservation lemmas.
+  - `Core/Question/Partition/Negativity.lean` (new, ~50 LOC): Merin's
+    epistemic characterization — `isProperCoarsening`,
+    `isNegativeAttribute`.
+- **DT block extracted to `Core/Agent/PartitionDT.lean`** (767 LOC) —
+  partition decision-theoretic infrastructure (`partitionEU`,
+  `eu_eq_partitionEU`, `coarsening_preserves_eu`, `partitionValue`,
+  Blackwell ordering theorems, `questionUtility_qud_nonneg`) lives
+  under `Core/Agent/` to mirror its dependency on
+  `Core/Agent/DecisionTheory.lean`.
+- Architectural choice: Direction A (Setoid-canonical) — `QUD`,
+  `Question`, and partition primitives are co-located construction /
+  consumption faces of the underlying `Setoid` rather than separately
+  unified. Mirrors mathlib's non-unification of `Setoid` + `LowerSet`
+  + `IsPartition`.
+- **21 consumers migrated** (Linglib.lean + 20 importers) across
+  `Theories/Semantics/Questions/`, `Theories/Semantics/Plurality/`,
+  `Theories/Semantics/Focus/`, `Theories/Pragmatics/Dialogue/KOS/`,
+  `Core/Discourse/`, and `Phenomena/Studies/`.
+
+### Fixed
+- **`Interval Time` `[LE Time]` → `[LinearOrder Time]` cascade**
+  (pre-existing build failure unrelated to partition work). The Time
+  directory rename in 0.230.99 (commit f64da888) tightened
+  `Interval Time` to require `[LinearOrder Time]`, but ~12 downstream
+  files declaring functions/structures over `Ev Time` /
+  `Eventuality Time` / `Interval Time` weren't propagated. Strengthened
+  at definition sites (safe — `LinearOrder` extends `LE`) in:
+  `Events/Basic.lean`, `Events/EventRelations.lean`,
+  `Events/DegreeEvents.lean` (also `[LE Deg]` → `[LinearOrder Deg]`),
+  `Events/ThematicRoles.lean`, `Attitudes/RationalAttitude.lean`,
+  `Tense/TemporalAdverbials.lean`, `Quotation/Demonstration.lean`,
+  `Morphology/ReversalRestitution.lean`,
+  `Phenomena/TenseAspect/Studies/Cruse1973.lean`,
+  `Phenomena/TenseAspect/Studies/OgiharaST2024.lean` (uses `T` rather
+  than `Time`), `Phenomena/Comparison/Studies/Wellwood2015.lean`,
+  `Phenomena/Gradability/Studies/CarianiSantorioWellwood2024.lean`,
+  `Phenomena/Quotation/Studies/Rudin2025LI.lean`. Files using only `≤`
+  (`Tense/Basic.lean::upperLimitConstraint`,
+  `Modality/TemporalConstraint.lean`, `Core/Modality/HistoricalAlternatives.lean`)
+  were left at `[LE Time]`.
+
 ## [0.230.107] - 2026-04-20
 
 ### Changed

Linglib.lean

@@ -60,7 +60,10 @@ import Linglib.Core.Semantics.PresuppositionContext
 import Linglib.Core.Semantics.Postsupposition
 import Linglib.Core.Semantics.ContentLayer
 import Linglib.Core.Agent.ProductOfExperts
-import Linglib.Core.Partition
+import Linglib.Core.Question.Partition.Lattice
+import Linglib.Core.Question.Partition.Cells
+import Linglib.Core.Question.Partition.Binary
+import Linglib.Core.Question.Partition.Negativity
 import Linglib.Core.Negation
 import Linglib.Core.Polarity
 import Linglib.Core.PolarityPartition
@@ -69,13 +72,13 @@ import Linglib.Core.Modality.ModalIndefinite
 import Linglib.Core.Modality.ModalBaseKind
 import Linglib.Core.Modality.ModalTypes
 import Linglib.Core.SelectionFunction
-import Linglib.Core.Question.QUD
+import Linglib.Core.Question.Partition.QUD
 import Linglib.Core.Question.PrecisionProjection
 import Linglib.Core.InfoState
 import Linglib.Core.Question.Support
 import Linglib.Core.Question.Basic
 import Linglib.Core.Question.Hamblin
-import Linglib.Core.Question.Partition
+import Linglib.Core.Question.Partition.Basic
 import Linglib.Core.Question.Singleton
 import Linglib.Core.Question.Answerhood
 import Linglib.Core.Question.Granularity
@@ -112,6 +115,7 @@ import Linglib.Core.Constraint.OT.Basic
 import Linglib.Core.Constraint.OT.ERC
 import Linglib.Core.Constraint.OT.Antimatroid
 import Linglib.Core.Agent.DecisionTheory
+import Linglib.Core.Agent.PartitionDT
 import Linglib.Core.Agent.BayesianUpdate
 import Linglib.Core.Agent.ExperimentDesign
 import Linglib.Core.Agent.RationalAction