What the tilted heart of a stability function is

HeartAdapter.lean produces hnTilt, a t-structure on C from a stability function on the heart and a cutoff β. It does not say what its heart contains. This file does, by specialising the Happel–Reiten–Smalø description already proved in TorsionPair/Heart.lean and Cohomology/Basic.lean:

A(β) = ⟨F β ⟦1⟧, T β⟩

• hnTilt_heart_iff — an object is in the tilted heart exactly when it sits in a distinguished triangle F₀⟦1⟧ → X → T₀ with all Harder–Narasimhan phases of F₀ at most β and all those of T₀ above it.
• mem_hnTilt_heart_of_hnTors, shift_mem_hnTilt_heart_of_hnFree — the two generating families, which are the T₀ = X and F₀⟦1⟧ = X ends of that triangle.

Nothing here is new mathematics; all three are one composition each. What they buy is that the tilted heart can be described in the phase language of Cutoff.lean rather than in terms of two abstract ObjectPropertys, which is the form §6 states it in.

Abelian/Stability/SlopeCutoff.lean is the companion on the other side: it says which objects are in T β to begin with, namely every nonzero object of rank zero, at every β < 1.

theorem CategoryTheory.Triangulated.StabilityFunction.hnTilt_heart_iff {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {t : TStructure C} (Z : StabilityFunction t.heart.FullSubcategory) (β : ℝ) (hHN : Z.HasHNProperty) (X : C) : (Z.hnTilt β hHN).heart X ↔ ∃ (F₀ : C) (T₀ : C) (_ : Tilting.ambientProperty t (Z.hnFreeProperty β) F₀) (_ : Tilting.ambientProperty t (Z.hnTorsProperty β) T₀) (f : (shiftFunctor C 1).obj F₀ ⟶ X) (g : X ⟶ T₀) (h : T₀ ⟶ (shiftFunctor C 1).obj ((shiftFunctor C 1).obj F₀)), Pretriangulated.Triangle.mk f g h ∈ Pretriangulated.distinguishedTriangles

The tilted heart is the extensions of T β by F β ⟦1⟧.

theorem CategoryTheory.Triangulated.StabilityFunction.mem_hnTilt_heart_of_hnTors {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {t : TStructure C} (Z : StabilityFunction t.heart.FullSubcategory) (β : ℝ) (hHN : Z.HasHNProperty) {T₀ : C} (hT : Tilting.ambientProperty t (Z.hnTorsProperty β) T₀) : (Z.hnTilt β hHN).heart T₀

A torsion object stays in the tilted heart.

theorem CategoryTheory.Triangulated.StabilityFunction.shift_mem_hnTilt_heart_of_hnFree {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {t : TStructure C} (Z : StabilityFunction t.heart.FullSubcategory) (β : ℝ) (hHN : Z.HasHNProperty) {F₀ : C} (hF : Tilting.ambientProperty t (Z.hnFreeProperty β) F₀) : (Z.hnTilt β hHN).heart ((shiftFunctor C 1).obj F₀)

A torsion-free object enters the tilted heart after one shift.