Property (3), p. 978 — split is monotone in its second argument

Proved

PaigeTarjan.Coarsest.split_monotone

by mikedeng1 · Sep 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

coarsest-partitionp2o-batch-p100bp2o-gran-per-chapterp2o-plan-paperp2o-v1partition-refinement

Let $E$ be a relation on a finite set $U$ , let $P$ and $Q$ be partitions of $U$ with $P$ a refinement of $Q$ , and let $S \subseteq U$ . Then

\mathrm{split}(S, P) \text{ is a refinement of } \mathrm{split}(S, Q).

Monotonicity of $\mathrm{split}$ is the step that carries the invariant of Lemma 2 from one refinement step to the next.

Preamble

import Mathlib
import Definitions.Def_PaigeTarjan_Coarsest_Basic

Formal statement

namespace PaigeTarjan.Coarsest

/-- Property (3), p. 978: `split` is monotone in its second argument — if `S ⊆ U` and `P` is a
refinement of `Q`, then `split(S, P)` is a refinement of `split(S, Q)`. -/
theorem split_monotone {U : Type*} [Fintype U] [DecidableEq U]
    (E : U → U → Prop) [DecidableRel E] (P Q : Finset (Finset U)) (S : Finset U)
    (hP : IsPartition P) (hQ : IsPartition Q) (hPQ : Refines P Q) :
    Refines (split E S P) (split E S Q) := by sorry

end PaigeTarjan.Coarsest

Source

Paige, Tarjan, Three Partition Refinement Algorithms, SIAM J. Comput. 16 (1987), p. 978, property (3)

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

Take a finite set $U$ with decidable equality, a decidable binary relation $E$ on $U$ , families $P$ and $Q$ of subsets of $U$ , and a set $S \subseteq U$ . Assume:

$P$ is a partition of $U$ ;
$Q$ is a partition of $U$ ;
$P$ refines $Q$ .

Then $\operatorname{split}(S, P)$ refines $\operatorname{split}(S, Q)$ : every block of $\operatorname{split}(S, P)$ lies inside some block of $\operatorname{split}(S, Q)$ . Here $\operatorname{split}(S, \cdot)$ replaces each block $B$ by the nonempty sets among $B \cap E^{-1}(S)$ and $B \setminus E^{-1}(S)$ , where $E^{-1}(S) = \{x : \exists y \in S,\ x \mathrel{E} y\}$ .

Degenerate cases. If $U = \varnothing$ , all families involved are empty and the claim is vacuous. If $S = \varnothing$ , splitting leaves both partitions unchanged, and the claim reduces to the hypothesis that $P$ refines $Q$ .

Human review

Endorsed by Shuze Chen · Sep 27, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Sep 27, 2026
Confirmed by the mission captain (proposal self-audit).

View graph