IndisputableMonolith.Numerics.Interval.GalacticBounds

   1import IndisputableMonolith.Numerics.Interval.Basic
   2import IndisputableMonolith.Numerics.Interval.Pow
   3import IndisputableMonolith.Constants
   4
   5namespace IndisputableMonolith.Numerics
   6
   7open Interval
   8open Real
   9
  10/-- Ratio τ★ / τ₀ ≈ 5.75e29 -/
  11def galactic_ratio_rational : ℚ := 41971608 * 10^24 / 73
  12
  13/-- φ^51 lo > 0 -/
  14lemma phi_pow_51_lo_pos : (0 : ℚ) < phi_pow_51_interval.lo := by
  15  unfold phi_pow_51_interval; norm_num
  16
  17/-- Interval for φ^102 = (φ^51)^2 -/
  18def phi_pow_102_interval : Interval :=
  19  mulPos phi_pow_51_interval phi_pow_51_interval phi_pow_51_lo_pos phi_pow_51_lo_pos
  20
  21/-- φ^16 lo > 0 -/
  22lemma phi_pow_16_lo_pos : (0 : ℚ) < phi_pow_16_interval.lo := by
  23  unfold phi_pow_16_interval; norm_num
  24
  25/-- φ^5 lo > 0 -/
  26lemma phi_pow_5_lo_pos : (0 : ℚ) < phi_pow_5_interval.lo := by
  27  unfold phi_pow_5_interval; norm_num
  28
  29/-- φ lo > 0 -/
  30lemma phi_lo_pos : (0 : ℚ) < phiInterval.lo := by
  31  unfold phiInterval; norm_num
  32
  33/-- Interval for φ^32 = (φ^16)^2 -/
  34def phi_pow_32_interval : Interval :=
  35  mulPos phi_pow_16_interval phi_pow_16_interval phi_pow_16_lo_pos phi_pow_16_lo_pos
  36
  37lemma phi_pow_32_lo_pos : (0 : ℚ) < phi_pow_32_interval.lo := by
  38  unfold phi_pow_32_interval mulPos; dsimp
  39  exact mul_pos phi_pow_16_lo_pos phi_pow_16_lo_pos
  40
  41/-- Interval for φ^37 = φ^32 * φ^5 -/
  42def phi_pow_37_interval : Interval :=
  43  mulPos phi_pow_32_interval phi_pow_5_interval phi_pow_32_lo_pos phi_pow_5_lo_pos
  44
  45lemma phi_pow_37_lo_pos : (0 : ℚ) < phi_pow_37_interval.lo := by
  46  unfold phi_pow_37_interval mulPos; dsimp
  47  exact mul_pos phi_pow_32_lo_pos phi_pow_5_lo_pos
  48
  49/-- Interval for φ^38 = φ^37 * φ^1 -/
  50def phi_pow_38_interval : Interval :=
  51  mulPos phi_pow_37_interval phiInterval phi_pow_37_lo_pos phi_lo_pos
  52
  53lemma phi_pow_102_lo_pos : (0 : ℚ) < phi_pow_102_interval.lo := by
  54  unfold phi_pow_102_interval mulPos; dsimp
  55  exact mul_pos phi_pow_51_lo_pos phi_pow_51_lo_pos
  56
  57lemma phi_pow_38_lo_pos : (0 : ℚ) < phi_pow_38_interval.lo := by
  58  unfold phi_pow_38_interval mulPos; dsimp
  59  exact mul_pos phi_pow_37_lo_pos phi_lo_pos
  60
  61/-- Interval for φ^140 = φ^102 * φ^38 -/
  62def phi_pow_140_interval : Interval :=
  63  mulPos phi_pow_102_interval phi_pow_38_interval phi_pow_102_lo_pos phi_pow_38_lo_pos
  64
  65lemma phi_pow_140_lo_pos : (0 : ℚ) < phi_pow_140_interval.lo := by
  66  unfold phi_pow_140_interval mulPos; dsimp
  67  exact mul_pos phi_pow_102_lo_pos phi_pow_38_lo_pos
  68
  69/-- Interval for φ^145 = φ^140 * φ^5 -/
  70def phi_pow_145_interval : Interval :=
  71  mulPos phi_pow_140_interval phi_pow_5_interval phi_pow_140_lo_pos phi_pow_5_lo_pos
  72
  73theorem phi_pow_140_in_interval : phi_pow_140_interval.contains (goldenRatio ^ (140 : ℝ)) := by
  74  have h_in_51 : phi_pow_51_interval.contains (goldenRatio ^ (51 : ℝ)) := phi_pow_51_in_interval
  75  have h_in_102 : phi_pow_102_interval.contains (goldenRatio ^ (102 : ℝ)) := by
  76    unfold phi_pow_102_interval
  77    have : goldenRatio ^ (102 : ℝ) = goldenRatio ^ (51 : ℝ) * goldenRatio ^ (51 : ℝ) := by
  78      rw [← Real.rpow_add goldenRatio_pos]; norm_num
  79    rw [this]
  80    apply mulPos_contains_mul phi_pow_51_lo_pos phi_pow_51_lo_pos h_in_51 h_in_51
  81
  82  have h_in_16 : phi_pow_16_interval.contains (goldenRatio ^ (16 : ℝ)) := phi_pow_16_in_interval
  83  have h_in_32 : phi_pow_32_interval.contains (goldenRatio ^ (32 : ℝ)) := by
  84    unfold phi_pow_32_interval
  85    have : goldenRatio ^ (32 : ℝ) = goldenRatio ^ (16 : ℝ) * goldenRatio ^ (16 : ℝ) := by
  86      rw [← Real.rpow_add goldenRatio_pos]; norm_num
  87    rw [this]
  88    apply mulPos_contains_mul phi_pow_16_lo_pos phi_pow_16_lo_pos h_in_16 h_in_16
  89
  90  have h_in_5 : phi_pow_5_interval.contains (goldenRatio ^ (5 : ℝ)) := phi_pow_5_in_interval
  91  have h_in_37 : phi_pow_37_interval.contains (goldenRatio ^ (37 : ℝ)) := by
  92    unfold phi_pow_37_interval
  93    have : goldenRatio ^ (37 : ℝ) = goldenRatio ^ (32 : ℝ) * goldenRatio ^ (5 : ℝ) := by
  94      rw [← Real.rpow_add goldenRatio_pos]; norm_num
  95    rw [this]
  96    apply mulPos_contains_mul phi_pow_32_lo_pos phi_pow_5_lo_pos h_in_32 h_in_5
  97
  98  have h_in_1 : phiInterval.contains goldenRatio := phi_in_phiInterval
  99  have h_in_38 : phi_pow_38_interval.contains (goldenRatio ^ (38 : ℝ)) := by
 100    unfold phi_pow_38_interval
 101    have : goldenRatio ^ (38 : ℝ) = goldenRatio ^ (37 : ℝ) * goldenRatio ^ (1 : ℝ) := by
 102      rw [← Real.rpow_add goldenRatio_pos]; norm_num
 103    rw [this, Real.rpow_one]
 104    apply mulPos_contains_mul phi_pow_37_lo_pos phi_lo_pos h_in_37 h_in_1
 105
 106  unfold phi_pow_140_interval
 107  have : goldenRatio ^ (140 : ℝ) = goldenRatio ^ (102 : ℝ) * goldenRatio ^ (38 : ℝ) := by
 108    rw [← Real.rpow_add goldenRatio_pos]; norm_num
 109  rw [this]
 110  apply mulPos_contains_mul phi_pow_102_lo_pos phi_pow_38_lo_pos h_in_102 h_in_38
 111
 112theorem phi_pow_145_in_interval : phi_pow_145_interval.contains (goldenRatio ^ (145 : ℝ)) := by
 113  have h_in_140 := phi_pow_140_in_interval
 114  have h_in_5 : phi_pow_5_interval.contains (goldenRatio ^ (5 : ℝ)) := phi_pow_5_in_interval
 115  unfold phi_pow_145_interval
 116  have : goldenRatio ^ (145 : ℝ) = goldenRatio ^ (140 : ℝ) * goldenRatio ^ (5 : ℝ) := by
 117    rw [← Real.rpow_add goldenRatio_pos]; norm_num
 118  rw [this]
 119  apply mulPos_contains_mul phi_pow_140_lo_pos phi_pow_5_lo_pos h_in_140 h_in_5
 120
 121/-- φ^140 < galactic_ratio -/
 122theorem phi_pow_140_lt_ratio : goldenRatio ^ (140 : ℝ) < (galactic_ratio_rational : ℝ) := by
 123  have h_in_140 := phi_pow_140_in_interval
 124  have h_hi : phi_pow_140_interval.hi < galactic_ratio_rational := by
 125    unfold phi_pow_140_interval phi_pow_102_interval phi_pow_38_interval phi_pow_37_interval phi_pow_32_interval phi_pow_51_interval phi_pow_16_interval phi_pow_5_interval phiInterval mulPos
 126    norm_num
 127  exact lt_of_le_of_lt h_in_140.2 (by exact_mod_cast h_hi)
 128
 129/-- galactic_ratio < φ^145 -/
 130theorem ratio_lt_phi_pow_145 : (galactic_ratio_rational : ℝ) < goldenRatio ^ (145 : ℝ) := by
 131  have h_in_145 := phi_pow_145_in_interval
 132  have h_lo : galactic_ratio_rational < phi_pow_145_interval.lo := by
 133    unfold phi_pow_145_interval phi_pow_140_interval phi_pow_102_interval phi_pow_38_interval phi_pow_37_interval phi_pow_32_interval phi_pow_51_interval phi_pow_16_interval phi_pow_5_interval phiInterval mulPos
 134    norm_num
 135  exact lt_of_lt_of_le (by exact_mod_cast h_lo) h_in_145.1
 136
 137/-- Interval for φ^2 = φ + 1 -/
 138def phi_pow_2_interval : Interval :=
 139  phiInterval.add (Interval.point 1)
 140
 141lemma phi_pow_2_lo_pos : (0 : ℚ) < phi_pow_2_interval.lo := by
 142  unfold phi_pow_2_interval phiInterval; norm_num
 143
 144/-- Interval for φ^142 = φ^140 * φ^2 -/
 145def phi_pow_142_interval : Interval :=
 146  mulPos phi_pow_140_interval phi_pow_2_interval phi_pow_140_lo_pos phi_pow_2_lo_pos
 147
 148theorem phi_pow_142_in_interval : phi_pow_142_interval.contains (goldenRatio ^ (142 : ℝ)) := by
 149  have h_in_140 := phi_pow_140_in_interval
 150  have h_in_2 : phi_pow_2_interval.contains (goldenRatio ^ (2 : ℝ)) := by
 151    unfold phi_pow_2_interval
 152    have h_sq : goldenRatio ^ (2 : ℝ) = goldenRatio + 1 := goldenRatio_sq
 153    rw [h_sq]
 154    apply add_contains_add (phi_in_phiInterval) (contains_point 1)
 155  unfold phi_pow_142_interval
 156  have : goldenRatio ^ (142 : ℝ) = goldenRatio ^ (140 : ℝ) * goldenRatio ^ (2 : ℝ) := by
 157    rw [← Real.rpow_add goldenRatio_pos]; norm_num
 158  rw [this]
 159  apply mulPos_contains_mul phi_pow_140_lo_pos phi_pow_2_lo_pos h_in_140 h_in_2
 160
 161theorem phi_pow_142_lt_ratio_1_3 : phi_pow_142_interval.hi < 13/10 * galactic_ratio_rational := by
 162  unfold phi_pow_142_interval phi_pow_2_interval phi_pow_140_interval phi_pow_102_interval phi_pow_38_interval phi_pow_37_interval phi_pow_32_interval phi_pow_51_interval phi_pow_16_interval phi_pow_5_interval phiInterval mulPos Interval.add Interval.point
 163  norm_num
 164
 165theorem ratio_0_7_lt_phi_pow_142 : 7/10 * galactic_ratio_rational < phi_pow_142_interval.lo := by
 166  unfold phi_pow_142_interval phi_pow_2_interval phi_pow_140_interval phi_pow_102_interval phi_pow_38_interval phi_pow_37_interval phi_pow_32_interval phi_pow_51_interval phi_pow_16_interval phi_pow_5_interval phiInterval mulPos Interval.add Interval.point
 167  norm_num
 168
 169end IndisputableMonolith.Numerics
 170