doubledZeroDefect_recurrence

formal source

  37
  38This is the concrete Phase 4 instantiation currently available: a one-step
  39self-composition law on doubled deviation. -/
  40theorem doubledZeroDefect_recurrence (ρ : ℂ) :
  41    doubledZeroDefect ρ = 2 * (zeroDefect ρ) ^ 2 + 4 * zeroDefect ρ := by
  42  rw [doubledZeroDefect_eq_cosh_sub_one, zeroDefect_eq_cosh_sub_one]
  43  rw [Real.cosh_two_mul]
  44  nlinarith [Real.cosh_sq (zeroDeviation ρ)]
  45
  46/-- The doubled zero defect is always nonnegative. -/
  47theorem doubledZeroDefect_nonneg (ρ : ℂ) : 0 ≤ doubledZeroDefect ρ := by
  48  rw [doubledZeroDefect_eq_cosh_sub_one]
  49  linarith [Real.one_le_cosh (2 * zeroDeviation ρ)]
  50
  51/-- Doubling the deviation still vanishes exactly on the critical line. -/
  52theorem doubledZeroDefect_zero_iff_on_critical_line (ρ : ℂ) :
  53    doubledZeroDefect ρ = 0 ↔ OnCriticalLine ρ := by
  54  rw [doubledZeroDefect_eq_cosh_sub_one]
  55  constructor
  56  · intro h
  57    have hz : 2 * zeroDeviation ρ = 0 := by
  58      by_contra hne
  59      have hgt : 1 < Real.cosh (2 * zeroDeviation ρ) := Real.one_lt_cosh.mpr hne
  60      linarith
  61    have hdev : zeroDeviation ρ = 0 := by linarith
  62    exact (zeroDeviation_eq_zero_iff_on_critical_line ρ).mp hdev
  63  · intro h
  64    have hdev : zeroDeviation ρ = 0 :=
  65      (zeroDeviation_eq_zero_iff_on_critical_line ρ).mpr h
  66    simp [hdev]
  67
  68/-- Packaging of the strongest currently instantiated Vector C data. -/
  69theorem current_vectorC_attempt_data (ρ : ℂ) :
  70    (zeroDefect ρ = 0 ↔ OnCriticalLine ρ) ∧