defectIterate_zero_pos

formal source

  68  linarith [Real.one_le_cosh ((2 : ℝ) ^ n * t)]
  69
  70/-- d₀ > 0 for t ≠ 0 (off the critical line). -/
  71theorem defectIterate_zero_pos {t : ℝ} (ht : t ≠ 0) : 0 < defectIterate t 0 := by
  72  rw [defectIterate_zero_eq_J_log]
  73  exact Foundation.DiscretenessForcing.J_log_pos ht
  74
  75/-! ## §2. The recurrence from the RCL -/
  76
  77/-- **The composition recurrence.**
  78
  79    dₙ₊₁ = 2 · dₙ · (dₙ + 2)
  80
  81    This is forced by the Recognition Composition Law: applying the
  82    RCL to the pair (e^{2ⁿt}, e^{−2ⁿt}) yields the cosh double-angle
  83    formula, which is exactly this recurrence.
  84
  85    Mathematical content:
  86      cosh(2·u) = 2cosh²(u) − 1
  87      ⟹ cosh(2u)−1 = 2(cosh u − 1)(cosh u + 1)
  88                    = 2·(cosh u − 1)·((cosh u − 1) + 2) -/
  89theorem defectIterate_succ (t : ℝ) (n : ℕ) :
  90    defectIterate t (n + 1) = 2 * defectIterate t n * (defectIterate t n + 2) := by
  91  simp only [defectIterate]
  92  rw [show (2 : ℝ) ^ (n + 1) * t = 2 * ((2 : ℝ) ^ n * t) from by rw [pow_succ]; ring]
  93  have hd := Real.cosh_two_mul ((2 : ℝ) ^ n * t)
  94  have hs := Real.cosh_sq ((2 : ℝ) ^ n * t)
  95  set c := Real.cosh ((2 : ℝ) ^ n * t)
  96  set s := Real.sinh ((2 : ℝ) ^ n * t)
  97  have lhs : Real.cosh (2 * ((2 : ℝ) ^ n * t)) - 1 = 2 * c ^ 2 - 2 := by linarith
  98  have rhs_eq : 2 * (c - 1) * (c - 1 + 2) = 2 * c ^ 2 - 2 := by ring
  99  linarith
 100
 101/-- The recurrence in "squared ratio" form: