Harder--Narasimhan mass for weak prestability conditions

The mass-uniqueness induction of Metric/Mass/Uniqueness.lean is stated for a bare carrier (s : Slicing C, Z : K₀ C →+ ℂ), precisely because it never consults a compatibility ray. A weak prestability condition carries both — a slicing and a charge whose ray is closed at integer phases — so its HN mass theory is the general one, instantiated. This file makes those instances the public weak API: the mass of a weak HN filtration is independent of the filtration, the choice-free envelope equals every filtration's finite sum, and the envelope is finite.

What does not transport is positivity: a nonzero weak semistable object of integer phase may have charge zero, so stabilityMass_pos has no weak analogue, and the zero-mass locus is exactly the A⁰ direction of Definition 14.3 rather than the zero objects. Nothing in this file claims otherwise.

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.hnMass {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Λ : Type u_2} [AddCommGroup Λ] {v : K₀ C →+ Λ} (W : WeakPreStabilityCondition v) {E : C} (F : HNFiltration C W.slicing.P E) : ENNReal

The finite mass sum of one HN filtration for the slicing of a weak prestability condition: the general classMass at the composite charge W.Z.comp v.

Equations

• W.hnMass F = CategoryTheory.Triangulated.HNFiltration.classMass (W.Z.comp v) F

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.stabilityMass {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Λ : Type u_2} [AddCommGroup Λ] {v : K₀ C →+ Λ} (W : WeakPreStabilityCondition v) (E : C) : ENNReal

The choice-free weak HN mass envelope of an object.

Equations

• W.stabilityMass E = W.slicing.classMass (W.Z.comp v) E

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.hnMass_eq_hnMass {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {Λ : Type u_2} [AddCommGroup Λ] {v : K₀ C →+ Λ} (W : WeakPreStabilityCondition v) {E : C} (F G : HNFiltration C W.slicing.P E) : W.hnMass F = W.hnMass G

Weak HN mass is independent of the chosen HN filtration. The head–tail octahedral induction never needs the charge of a semistable factor to be nonzero, so it applies verbatim to the closed compatibility ray.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.stabilityMass_eq_hnMass {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {Λ : Type u_2} [AddCommGroup Λ] {v : K₀ C →+ Λ} (W : WeakPreStabilityCondition v) {E : C} (F : HNFiltration C W.slicing.P E) : W.stabilityMass E = W.hnMass F

The weak mass envelope is the finite mass sum of every HN filtration.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.stabilityMass_ne_top {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {Λ : Type u_2} [AddCommGroup Λ] {v : K₀ C →+ Λ} (W : WeakPreStabilityCondition v) (E : C) : W.stabilityMass E ≠ ⊤

The weak mass envelope is always finite. Finiteness needs only that some HN filtration exists and that each filtration's mass is a finite sum — never positivity of the summands, which is what fails weakly.