Global truncation for the owner deformed phase cuts

Every object is split into old high, middle, and low phase pieces. The high and low pieces enter the corresponding deformed cuts by the two-radius embedding lemmas. The middle piece lies in one of the uniformly finite wide sectors and therefore has an owner deformed HN filtration. Two uses of the octahedral axiom assemble the three pieces.

theorem CategoryTheory.Triangulated.StabilityCondition.WithClassMap.exists_global_deformedCut_triangle (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {Λ : Type u'} [AddCommGroup Λ] {κ : K₀ C →+ Λ} (σ : WithClassMap C κ) (W : Λ →+ ℂ) {r : ℝ} (hr0 : 0 ≤ r) (hr1 : r < 1) (hW : WeakStabilityCondition.StabilityCondition.Deformation.stabilitySeminorm C σ (W - σ.Z) ≤ ENNReal.ofReal r) {ε₀ : ℝ} (hε₀16 : ε₀ < 1 / 16) (hWide : WeakStabilityCondition.StabilityCondition.Deformation.WideSectorFiniteLength C σ ε₀) {ε : ℝ} (hε : 0 < ε) (hεhalf : ε < ε₀ / 2) (hε2 : ε ≤ 1 / 2) (hε8 : ε < 1 / 8) (hsin : WeakStabilityCondition.StabilityCondition.Deformation.stabilitySeminorm C σ (W - σ.Z) < ENNReal.ofReal (Real.sin (Real.pi * ε))) (E : C) (t : ℝ) : ∃ (X : C) (Y : C) (f : X ⟶ E) (g : E ⟶ Y) (δ : Y ⟶ (shiftFunctor C 1).obj X), Pretriangulated.Triangle.mk f g δ ∈ Pretriangulated.distinguishedTriangles ∧ deformedGtPred C σ W hr0 hr1 hW ε t X ∧ deformedLePred C σ W hr0 hr1 hW ε t Y

Every object has a truncation triangle for the owner provisional deformed phase cuts.