Owner phase truncation at an arbitrary real cutoff

Translate an owner HN filtration so a real cutoff becomes zero, apply the owner zero-cut truncation, and translate the two phase-cut memberships back.

theorem CategoryTheory.Triangulated.Slicing.exists_cutoff_truncation (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] (s : Slicing C) {A : C} (F : HNFiltration C s.P A) (t : ℝ) : ∃ (X : C) (Y : C) (_ : gtProp C s t X) (_ : leProp C s t Y) (f : X ⟶ A) (g : A ⟶ Y) (h : Y ⟶ (shiftFunctor C 1).obj X), Pretriangulated.Triangle.mk f g h ∈ Pretriangulated.distinguishedTriangles

Every owner HN filtration admits a distinguished truncation triangle at an arbitrary real phase cutoff.

theorem CategoryTheory.Triangulated.Slicing.exists_cutoff_truncation_in_interval (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] (s : Slicing C) {A : C} (F : HNFiltration C s.P A) {a b t : ℝ} (hA : intervalProp C s a b A) (hat : a ≤ t) (htb : t < b) : ∃ (X : C) (Y : C) (_ : gtProp C s t X) (_ : leProp C s t Y) (_ : intervalProp C s a b X) (_ : intervalProp C s a b Y) (f : X ⟶ A) (g : A ⟶ Y) (h : Y ⟶ (shiftFunctor C 1).obj X), Pretriangulated.Triangle.mk f g h ∈ Pretriangulated.distinguishedTriangles

Truncating an object at a cutoff inside an old phase interval keeps both pieces in that interval.