Reverse weak heart--slicing assembly for the phase tilt

This module connects the heart-level output of TiltAssembly to the reverse weak heart--slicing foundations. The analytic ray identity is supplied by ChargeRay: normalized weak slopes give the required heart charge rays, and integer shifts give the ambient compatibility axiom.

Hom vanishing is discharged by HeartHomVanishing, and ambient HN existence by AmbientHarderNarasimhan: boundedness of the tilted t-structure and the heart HN property extend the towers through the finite t-cohomological filtration. Consequently the phase-language weak upper tilt is now packaged without an external reverse-equivalence premise. The exact slope-language adapter and source-normalized theorem are exposed separately by Tilting/Source; this infrastructure alone makes no coverage promotion.

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.phaseTiltLatticeCharge {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {V : Type u_2} [NormedAddCommGroup V] {v : K₀ C →+ V} (sigma : WeakPreStabilityCondition v) (beta : ℝ) : V →+ ℂ

The lattice-level central charge of the phase tilt.

Equations

• sigma.phaseTiltLatticeCharge beta = (CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.phaseTiltRotation beta).comp sigma.Z

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.phaseTiltLatticeCharge_apply {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {V : Type u_2} [NormedAddCommGroup V] {v : K₀ C →+ V} (sigma : WeakPreStabilityCondition v) (beta : ℝ) (x : V) : (sigma.phaseTiltLatticeCharge beta) x = sigma.Z x * Complex.exp (-(↑Real.pi * ↑beta) * Complex.I)

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.phaseTilt_ambientPhasePredicate_charge_ray {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] {V : Type u_2} [NormedAddCommGroup V] {v : K₀ C →+ V} (sigma : WeakPreStabilityCondition v) (beta : ℝ) (hbeta0 : 0 ≤ beta) (hbeta1 : beta < 1) (phi : ℝ) (E : C) : (sigma.phaseTiltWeakStabilityFunction beta hbeta0 hbeta1).ambientPhasePredicate phi E → ¬Limits.IsZero E → ∃ (m : ℝ), 0 ≤ m ∧ ((∀ (n : ℤ), phi ≠ ↑n) → 0 < m) ∧ (sigma.phaseTiltLatticeCharge beta) (v (K₀.of C E)) = ↑m * Complex.exp (↑Real.pi * ↑phi * Complex.I)

The normalized ambient weak phase lies on the ray of the rotated lattice charge.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.PhaseTiltHeartObligations.ambientHN_exists_of_mem_tiltedHeart {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] {V : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] {v : K₀ C →+ V} (sigma : WeakPreStabilityCondition v) (beta : ℝ) (hbeta0 : 0 ≤ beta) (hbeta1 : beta < 1) (Zlin : V →ₗ[ℝ] ℂ) (H : sigma.PhaseTiltHeartObligations beta hbeta0 hbeta1 Zlin) (E : C) (hE : (slicingTorsionPair sigma.slicing hbeta0 ⋯).tilt.heart E) : Nonempty (HNFiltration C (sigma.phaseTiltWeakStabilityFunction beta hbeta0 hbeta1).ambientPhasePredicate E)

The heart-level HN field of the phase-tilt assembly gives ambient HN towers for all objects already lying in the tilted heart.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.PhaseTiltHeartObligations.ambientHN {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] {V : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] {v : K₀ C →+ V} (sigma : WeakPreStabilityCondition v) (beta : ℝ) (hbeta0 : 0 ≤ beta) (hbeta1 : beta < 1) (Zlin : V →ₗ[ℝ] ℂ) (H : sigma.PhaseTiltHeartObligations beta hbeta0 hbeta1 Zlin) (E : C) : Nonempty (HNFiltration C (sigma.phaseTiltWeakStabilityFunction beta hbeta0 hbeta1).ambientPhasePredicate E)

The heart HN field of the phase-tilt assembly extends canonically to an ambient HN filtration for every object. Boundedness of the original slicing t-structure is preserved by the HRS tilt, and WeakStabilityFunction.ambientHN_exists_of_bounded performs the finite t-cohomological assembly.

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.PhaseTiltHeartObligations.toWeakPreStabilityCondition {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] {V : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] {v : K₀ C →+ V} {sigma : WeakPreStabilityCondition v} {beta : ℝ} {hbeta0 : 0 ≤ beta} {hbeta1 : beta < 1} {Zlin : V →ₗ[ℝ] ℂ} (H : sigma.PhaseTiltHeartObligations beta hbeta0 hbeta1 Zlin) : WeakPreStabilityCondition v

Package the completed heart-level phase-tilt assembly as an ambient weak prestability condition. Both ambient HN existence and charge-ray compatibility are derived rather than supplied as premises.

Equations

• H.toWeakPreStabilityCondition = ⋯.toWeakPreStabilityCondition (sigma.phaseTiltLatticeCharge beta) ⋯

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.PhaseTiltHeartObligations.toWeakPreStabilityCondition_Z {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] {V : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] {v : K₀ C →+ V} {sigma : WeakPreStabilityCondition v} {beta : ℝ} {hbeta0 : 0 ≤ beta} {hbeta1 : beta < 1} {Zlin : V →ₗ[ℝ] ℂ} (H : sigma.PhaseTiltHeartObligations beta hbeta0 hbeta1 Zlin) : H.toWeakPreStabilityCondition.Z = sigma.phaseTiltLatticeCharge beta

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.PhaseTiltHeartObligations.toWeakPreStabilityCondition_P {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] {V : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] {v : K₀ C →+ V} {sigma : WeakPreStabilityCondition v} {beta : ℝ} {hbeta0 : 0 ≤ beta} {hbeta1 : beta < 1} {Zlin : V →ₗ[ℝ] ℂ} (H : sigma.PhaseTiltHeartObligations beta hbeta0 hbeta1 Zlin) : H.toWeakPreStabilityCondition.slicing.P = (sigma.phaseTiltWeakStabilityFunction beta hbeta0 hbeta1).ambientPhasePredicate

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.phaseTiltWeakPreStabilityConditionOfTiltingProperty {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] {V : Type u_2} [NormedAddCommGroup V] {v : K₀ C →+ V} (sigma : WeakPreStabilityCondition v) (beta : ℝ) (hbeta0 : 0 < beta) (hbeta1 : beta < 1) (htilt : sigma.TiltingProperty) : WeakPreStabilityCondition v

The phase-language weak upper tilt constructed directly from Definition 14.12's tilting property. The HN and charge-ray inputs are derived directly; no support-property realization is needed to construct the ambient weak prestability condition. This declaration deliberately makes no claim that the exact slope-language statement of Proposition 14.16 has been reviewed.

Equations

• sigma.phaseTiltWeakPreStabilityConditionOfTiltingProperty beta hbeta0 hbeta1 htilt = ⋯.toWeakPreStabilityCondition (sigma.phaseTiltLatticeCharge beta) ⋯

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.phaseTiltWeakPreStabilityConditionOfTiltingProperty_Z {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] {V : Type u_2} [NormedAddCommGroup V] {v : K₀ C →+ V} (sigma : WeakPreStabilityCondition v) (beta : ℝ) (hbeta0 : 0 < beta) (hbeta1 : beta < 1) (htilt : sigma.TiltingProperty) : (sigma.phaseTiltWeakPreStabilityConditionOfTiltingProperty beta hbeta0 hbeta1 htilt).Z = sigma.phaseTiltLatticeCharge beta

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.phaseTiltWeakPreStabilityConditionOfTiltingProperty_P {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] {V : Type u_2} [NormedAddCommGroup V] {v : K₀ C →+ V} (sigma : WeakPreStabilityCondition v) (beta : ℝ) (hbeta0 : 0 < beta) (hbeta1 : beta < 1) (htilt : sigma.TiltingProperty) : (sigma.phaseTiltWeakPreStabilityConditionOfTiltingProperty beta hbeta0 hbeta1 htilt).slicing.P = (sigma.phaseTiltWeakStabilityFunction beta ⋯ hbeta1).ambientPhasePredicate