gapDiff_eq

formal source

  73
  74theorem gapLCM_eq : gapLCM = 360 := by native_decide
  75
  76theorem gapDiff_eq : gapDiff = 37 := by native_decide
  77
  78/-- The beat is prime, and therefore coprime with every proper
  79    divisor of the 360-tick window. -/
  80theorem gapDiff_prime : Nat.Prime gapDiff := by
  81  rw [gapDiff_eq]; exact beat_is_prime
  82
  83/-- The two Gap-45 primitives are coprime, which is the hypothesis
  84    that generates the whole barrier. -/
  85theorem gap_coprime : Nat.Coprime bodyPeriod gapPeriod := coprime_barrier
  86
  87/-! ## The Shimmer factor -/
  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`