No essential bar is born at a non-critical level: mult(rankFn)(b, ⊥) = 0
ProvedPersistClust.Count.noncritical_level_mult_zeroLet ι 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. If b is a real level outside the critical set (hb : b ∉ (critSet hTame : Set ℝ)), then the multiplicity of the vertical bar born at b is zero: mult (rankFn stage J) ((b : EReal), (⊥ : EReal)) = 0. Proof sketch: the multiplicity at (b, ⊥) is the infimum over ε > 0 and t ≤ b − ε of the difference rankFn (b − ε) t − rankFn (b + ε) t; since every cell's birth-supremum lies in the critical set, a δ₀-gap around b excludes all birth-sups from the window (b − δ₀/2, b + δ₀/2), so at t = b − 1 the window-split rank identity gives rankFn (b − δ₀/2) (b − 1) − rankFn (b + δ₀/2) (b − 1) = encard of the empty set = 0 (using the ℕ∞ subtraction cancellation with the finiteness of the ranks from q-tameness); the infimum over all (ε, t) is then ≤ 0, and being an encard difference it is ≥ 0, hence 0. Birth levels of essential bars are therefore always critical.
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 noncritical_level_mult_zero {ι : Type*} {stage : ℝ → Set ι} {J : ℝ → ι → ι → Prop}
(hLaw : FiltrationLaw stage J) (hTame : IsTameModule stage J) {b : ℝ}
(hb : b ∉ (critSet hTame : Set ℝ)) :
mult (rankFn stage J) ((b : EReal), (⊥ : EReal)) = 0
:= by sorry