Window-β bridge: a cell is counted in the b-band iff its birth-supremum equals b
ProvedPersistClust.Count.win_beta_birth_pinLet ι be a type, stage : ℝ → Set ι a stage family and J : ℝ → ι → ι → Prop a relation family satisfying the filtration law hLaw and the tameness module axioms hTame. Let v be a level, C a v-cell, b a real level and η a positive radius such that every critical level τ ≠ b satisfies η < |τ − b| (the gap hypothesis: the closed η-window around b contains no critical level other than possibly b itself). Then C belongs to the b-band — the set of v-cells whose birth-supremum lies in the open window (b − η, b + η) — if and only if the birth-supremum of C is exactly b. Forward: every cell's birth-supremum is a critical level (unconditionally), and the gap hypothesis rules out every critical value other than b from the window, so a birth-supremum in the window must be b. Backward: b itself lies in the window since 0 < η. This is the membership bridge that converts band censuses into pinned β = b censuses in the matching-census assembly.
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
namespace PersistClust.Count
theorem win_beta_birth_pin {ι : Type*} {stage : ℝ → Set ι} {J : ℝ → ι → ι → Prop}
(hLaw : FiltrationLaw stage J) (hTame : IsTameModule stage J)
{v : ℝ} (C : comps stage J v) (b η : ℝ) (hη0 : 0 < η)
(hgap : ∀ τ ∈ critSet hTame, τ ≠ b → η < |τ - b|) :
C ∈ ({C : comps stage J v | b - η < birthSup hLaw v C ∧ birthSup hLaw v C < b + η} :
Set (comps stage J v)) ↔ birthSup hLaw v C = b
:= by sorry