Merge-count monotonicity: |S| + |g(S')| <= |S'| + |g(S)| for S a subset of S' (the functional |S| - |g(S)| is monotone)

Proved

PersistClust.Count.merge_count_mono

by fabianroll · Oct 15, 2026 · Mathlib 0df444a (Lean v4.33.1)

countencardgenericimageinduced-matchingmergemonotonepersistclustsupport-tool

Let g : U -> W be any map and S a subset of S' subsets of U. Then encard S + encard (g '' S') <= encard S' + encard (g '' S). Equivalently (for finite sets) the merge-count functional f(S) = |S| - |g(S)| -- the number of elements of S collapsed by g -- is monotone under inclusion: each added element raises |S| by one and |g(S)| by at most one. Stated additively in extended naturals, so no finiteness is needed.

Preamble

import Mathlib

Formal statement

namespace PersistClust.Count

theorem merge_count_mono {U W : Type*} (g : U → W) {S S' : Set U} (h : S ⊆ S') :
    S.encard + (g '' S').encard ≤ S'.encard + (g '' S).encard
    := by sorry

Source

Support tool of the persistence-clustering deliverable (RR-6968, Theorem 4.5 / 4.8 cluster): the counting core of the Bauer-Lesnick induced-matching route for 0-dimensional persistence, where g is a structure (merge) map between component sets and f(S_L) - f(S_R) counts the bars born in a window that die across the merge level. Pure Mathlib.

View graph