vei_step_ratio

formal source

  49
  50/-- The eruption recurrence ratio between adjacent VEI classes:
  51    `φ²`. -/
  52def vei_step_ratio : ℝ := phi ^ 2
  53
  54theorem vei_step_ratio_pos : 0 < vei_step_ratio := by
  55  unfold vei_step_ratio
  56  exact pow_pos phi_pos _
  57
  58/-- Numerical band: `vei_step_ratio = φ² ∈ (2.59, 2.63)`. -/
  59theorem vei_step_ratio_band :
  60    2.59 < vei_step_ratio ∧ vei_step_ratio < 2.63 := by
  61  unfold vei_step_ratio
  62  have h1 := Constants.phi_gt_onePointSixOne
  63  have h2 := phi_lt_onePointSixTwo
  64  have hpos : 0 < phi := phi_pos
  65  refine ⟨?_, ?_⟩
  66  · have : (1.61 : ℝ)^2 < phi^2 :=
  67      pow_lt_pow_left₀ h1 (by norm_num) (by norm_num)
  68    nlinarith
  69  · have : phi^2 < (1.62 : ℝ)^2 :=
  70      pow_lt_pow_left₀ h2 (le_of_lt hpos) (by norm_num)
  71    nlinarith
  72
  73/-! ## §2. Cumulative ratio across k steps -/
  74
  75/-- The cumulative recurrence ratio across `k` VEI steps:
  76    `φ^(2k)`. -/
  77def cumulative_ratio (k : ℕ) : ℝ := phi ^ (2 * k)
  78
  79theorem cumulative_ratio_pos (k : ℕ) : 0 < cumulative_ratio k := by
  80  unfold cumulative_ratio
  81  exact pow_pos phi_pos _
  82