Phase geometry for owner stability functions

The phase see-saw for a short exact sequence in an abelian category, read off the neutral half-plane argument bounds in Analysis/Complex/PhaseGeometry.lean.

Those bounds -- phaseCross, arg_add_le_max, min_arg_le_arg_add, arg_add_lt_max and the half-plane closure facts under them -- used to be declared here. They say nothing about categories, and MO1.13 (#1324) moved them to their neutral owner so that the Euclidean core of the mass-subadditivity proof could reach them without reaching stability. This file keeps the StabilityFunction statements, which genuinely need an abelian category.

theorem CategoryTheory.Triangulated.StabilityFunction.phase_le_max_of_shortExact {A : Type u} [Category.{v, u} A] [Abelian A] (Z : StabilityFunction A) (S : ShortComplex A) (hS : S.ShortExact) (h₁ : ¬Limits.IsZero S.X₁) (h₃ : ¬Limits.IsZero S.X₃) : Z.phase S.X₂ ≤ max (Z.phase S.X₁) (Z.phase S.X₃)

Upper phase see-saw for a short exact sequence.

theorem CategoryTheory.Triangulated.StabilityFunction.min_phase_le_of_shortExact {A : Type u} [Category.{v, u} A] [Abelian A] (Z : StabilityFunction A) (S : ShortComplex A) (hS : S.ShortExact) (h₁ : ¬Limits.IsZero S.X₁) (h₃ : ¬Limits.IsZero S.X₃) : min (Z.phase S.X₁) (Z.phase S.X₃) ≤ Z.phase S.X₂

Lower phase see-saw for a short exact sequence.

theorem CategoryTheory.Triangulated.StabilityFunction.phase_le_of_epi {A : Type u} [Category.{v, u} A] [Abelian A] (Z : StabilityFunction A) {E Q : A} (p : E ⟶ Q) [Epi p] (hE : Z.IsSemistable E) (hQ : ¬Limits.IsZero Q) : Z.phase E ≤ Z.phase Q

A nonzero quotient of a semistable object has phase at least the source phase.

theorem CategoryTheory.Triangulated.StabilityFunction.hom_eq_zero_of_semistable_phase_gt {A : Type u} [Category.{v, u} A] [Abelian A] (Z : StabilityFunction A) {E F : A} (hE : Z.IsSemistable E) (hF : Z.IsSemistable F) (hphase : Z.phase F < Z.phase E) (f : E ⟶ F) : f = 0

Hom-vanishing between semistable objects of decreasing phase.