shimmerFactor

formal source

  88
  89/-- The Shimmer subjective-time factor. Defined directly from the two
  90    Gap-45 primitives as `lcm(8,45) / (45 - 8)`. -/
  91def shimmerFactor : ℝ := (gapLCM : ℝ) / (gapDiff : ℝ)
  92
  93/-- The factor reduces to the bare arithmetic ratio `360 / 37`. -/
  94theorem shimmerFactor_eq_360_div_37 : shimmerFactor = (360 : ℝ) / 37 := by
  95  unfold shimmerFactor
  96  have h1 : (gapLCM : ℝ) = 360 := by exact_mod_cast gapLCM_eq
  97  have h2 : (gapDiff : ℝ) = 37 := by exact_mod_cast gapDiff_eq
  98  rw [h1, h2]
  99
 100theorem shimmerFactor_pos : 0 < shimmerFactor := by
 101  rw [shimmerFactor_eq_360_div_37]; norm_num
 102
 103theorem shimmerFactor_gt_one : 1 < shimmerFactor := by
 104  rw [shimmerFactor_eq_360_div_37]; norm_num
 105
 106/-! ## Numerical bounds: `~ 9.73`
 107
 108The approximation `9.73` is accurate to the displayed precision:
 109`360/37 = 9.72972972…`, so the factor sits strictly between
 110`9.72` and `9.73`. -/
 111
 112theorem shimmerFactor_gt_9_72 : (9.72 : ℝ) < shimmerFactor := by
 113  rw [shimmerFactor_eq_360_div_37]; norm_num
 114
 115theorem shimmerFactor_lt_9_73 : shimmerFactor < (9.73 : ℝ) := by
 116  rw [shimmerFactor_eq_360_div_37]; norm_num
 117
 118theorem shimmerFactor_approx :
 119    (9.72 : ℝ) < shimmerFactor ∧ shimmerFactor < (9.73 : ℝ) :=
 120  ⟨shimmerFactor_gt_9_72, shimmerFactor_lt_9_73⟩
 121