rungPhaseDelay_band

formal source

 106band `(0.481, 0.482)` requires `log_two_near_10` plus `log 1.25`
 107bounds; this looser band is sufficient to falsify against any
 108non-φ rung-phase delay. -/
 109theorem rungPhaseDelay_band :
 110    (0.30 : ℝ) < rungPhaseDelay ∧ rungPhaseDelay < 0.70 := by
 111  unfold rungPhaseDelay
 112  refine ⟨?_, ?_⟩
 113  · -- log φ > 0.30: from 2 log φ = log (phi^2) > log 2.5 > log 2 > 0.6931
 114    have hsq : (2 : ℝ) < phi ^ 2 := by
 115      have hb := phi_squared_bounds
 116      linarith
 117    have hlog : Real.log 2 < Real.log (phi ^ 2) :=
 118      Real.log_lt_log (by norm_num) hsq
 119    rw [Real.log_pow] at hlog
 120    push_cast at hlog
 121    have hlog2 : (0.69 : ℝ) < Real.log 2 := by
 122      have := Real.log_two_gt_d9
 123      linarith
 124    linarith
 125  · -- log φ < 0.70: from φ < 2 ⇒ log φ < log 2 < 0.6932
 126    have h1 : Real.log phi < Real.log 2 :=
 127      Real.log_lt_log phi_pos phi_lt_two
 128    have h2 : Real.log 2 < (0.6932 : ℝ) := by
 129      have := Real.log_two_lt_d9
 130      linarith
 131    linarith
 132
 133/-- RS echo delay for a bounce at radius `r_min`: `Δt = 2 r_min log φ`. -/
 134def echoDelay (r_min : ℝ) : ℝ := 2 * r_min * rungPhaseDelay
 135
 136theorem echoDelay_pos (r_min : ℝ) (h : 0 < r_min) :
 137    0 < echoDelay r_min := by
 138  unfold echoDelay
 139  have hpos := rungPhaseDelay_pos