Property (1), p. 978 — stability is inherited under refinement

Proved

PaigeTarjan.Coarsest.stableWrt_of_refines

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 $R$ be partitions of $U$ with $R$ a refinement of $P$ , and let $S \subseteq U$ . If $P$ is stable with respect to $S$ , then so is $R$ :

R \text{ refines } P,\ P \text{ stable w.r.t. } S \implies R \text{ stable w.r.t. } S.

This is why a set, once used as a splitter, can never be used as a splitter again: every later partition refines the one that was made stable with respect to it.

Preamble

import Mathlib
import Definitions.Def_PaigeTarjan_Coarsest_Basic

Formal statement

namespace PaigeTarjan.Coarsest

/-- Property (1), p. 978: stability is inherited under refinement — if `R` is a refinement of
`P` and `P` is stable with respect to a set `S`, then so is `R`. -/
theorem stableWrt_of_refines {U : Type*} [Fintype U] [DecidableEq U]
    (E : U → U → Prop) [DecidableRel E] (P R : Finset (Finset U)) (S : Finset U)
    (hP : IsPartition P) (hR : IsPartition R) (hRP : Refines R P)
    (hPS : StableWrt E P S) :
    StableWrt E R S := by sorry

end PaigeTarjan.Coarsest

Source

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

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 $R$ of subsets of $U$ , and a set $S \subseteq U$ . Assume:

$P$ is a partition of $U$ ;
$R$ is a partition of $U$ ;
$R$ refines $P$ , meaning every block of $R$ lies inside some block of $P$ ;
$P$ is stable with respect to $S$ , meaning every block $B \in P$ satisfies $B \subseteq E^{-1}(S)$ or $B \cap E^{-1}(S) = \varnothing$ , where $E^{-1}(S) = \{x : \exists y \in S,\ x \mathrel{E} y\}$ .

Then $R$ is stable with respect to $S$ : every block $C \in R$ satisfies $C \subseteq E^{-1}(S)$ or $C \cap E^{-1}(S) = \varnothing$ .

Degenerate cases. If $U = \varnothing$ , both partitions are empty and the conclusion holds vacuously. If $S = \varnothing$ , then $E^{-1}(S) = \varnothing$ and every family is stable with respect to $S$ .

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