The coarsening map at a reflexive order-relation is the identity

Proved

PersistClust.Count.struct_map_id

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

componentscountidentitypersistclustpersistencestructmapsupport-tool

Let ι be a type, stage : ℝ → Set ι a stage family and J : ℝ → ι → ι → Prop a relation family satisfying the filtration law hLaw. For every level t and every t-cell C, the structure map at the reflexive order-relation t ≤ t is the identity: structMap hLaw le_rfl C = C. Proof: structMap sends a cell to the t-class of its chosen representative (compRep), and compRep_spec states that the representative's class is exactly the cell's underlying set; Subtype.ext transports that set equality to equality of components. This trivial-seeming lemma is the anchor that makes the cell's own level an ancestor level of itself, used at the base of every ancestor-set nonemptiness argument in the birth-supremum machinery.

Preamble

import Mathlib
import Definitions.Def_PersistClust_Count_Setting
import Definitions.Def_PersistClust_Count_Diagram
import Definitions.Def_PersistClust_Count_FiltrationLaw
import Definitions.Def_PersistClust_Count_MatchingCensus

open PersistClust.Count
open scoped ENNReal

Formal statement

namespace PersistClust.Count

theorem struct_map_id {ι : Type*} {stage : ℝ → Set ι} {J : ℝ → ι → ι → Prop}
    (hLaw : FiltrationLaw stage J) (t : ℝ) (C : comps stage J t) :
    structMap hLaw le_rfl C = C
    := by sorry

Source

Support theorem of the persistence-clustering deliverable (RR-6968, Theorem 4.6 cluster): the structMap identity at le_rfl (t3_structMap_id in the rankKill master, Scratch_rankR1 L493-496, no in-file helpers) — consumed by the ancestor-set nonemptiness steps of the meets/rank/birth-sup machinery of the matching-census assembly.

View graph