Charge rays from normalized weak slopes

This module proves the analytic compatibility omitted from the reverse weak heart--slicing construction. The normalization

weakPhaseOfSlope μ = arctan μ / π + 1 / 2

puts every weak upper-half-plane charge on its corresponding phase ray. The finite-slope case has positive radius. At the infinite-slope boundary the charge lies on the nonpositive real axis and the radius may vanish, exactly as allowed at integer phases by WeakPreStabilityCondition.

The heart-level identity is then transported through arbitrary integer shifts. This supplies charge-ray compatibility for the ambient phase family constructed from any weak stability function, independently of tilting.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.complex_eq_pos_mul_exp_weakPhaseOfSlope (z : ℂ) (him : 0 < z.im) : ∃ (m : ℝ), 0 < m ∧ z = ↑m * Complex.exp (↑Real.pi * ↑(weakPhaseOfSlope ↑(-z.re / z.im)) * Complex.I)

A complex number in the open upper half-plane lies on the ray determined by its normalized weak slope, with positive radius.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakStabilityFunction.charge_ray_of_mem_heart {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {t : TStructure C} (W : WeakStabilityFunction t) (E : C) (hEheart : t.heart E) (hE0 : ¬Limits.IsZero E) : ∃ (m : ℝ), 0 ≤ m ∧ ((∀ (n : ℤ), W.phase E ≠ ↑n) → 0 < m) ∧ W.charge E = ↑m * Complex.exp (↑Real.pi * ↑(W.phase E) * Complex.I)

The charge of every nonzero heart object lies on the ray determined by its normalized weak phase. The radius is positive away from integer phases; at the phase-1 boundary it is merely nonnegative.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.negOnePow_mul_exp_pi_eq_exp_add_int (psi : ℝ) (n : ℤ) : ↑((-1) ^ n.natAbs) * Complex.exp (↑Real.pi * ↑psi * Complex.I) = Complex.exp (↑Real.pi * (↑psi + ↑↑n) * Complex.I)

Multiplication by the shift-parity sign advances a phase ray by the corresponding integer.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakStabilityFunction.ambientPhasePredicate_charge_ray {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {t : TStructure C} (W : WeakStabilityFunction t) (phi : ℝ) (E : C) (hP : W.ambientPhasePredicate phi E) (hE0 : ¬Limits.IsZero E) : ∃ (m : ℝ), 0 ≤ m ∧ ((∀ (n : ℤ), phi ≠ ↑n) → 0 < m) ∧ W.charge E = ↑m * Complex.exp (↑Real.pi * ↑phi * Complex.I)

The integer-normalized ambient phase predicate constructed from a weak stability function satisfies the charge-ray axiom of a weak prestability condition.