phi_suppression_bounded

formal source

  66
  67/-- **THEOREM EA-003.3**: The φ-suppression is bounded.
  68    φ^(-4.5) ∈ (0, 1) -/
  69theorem phi_suppression_bounded : phi_suppression_ga > 0 ∧ phi_suppression_ga < 1 := by
  70  have heq : phi_suppression_ga = phi ^ (-4.5 : ℝ) := by
  71    unfold phi_suppression_ga gallium_rung
  72    norm_num
  73  rw [heq]
  74  have h1 : phi ^ (-4.5 : ℝ) > 0 := by
  75    apply Real.rpow_pos_of_pos
  76    exact phi_pos
  77  have h2 : phi ^ (-4.5 : ℝ) < 1 := by
  78    -- phi^(-4.5) = 1/phi^4.5 and phi^4.5 > 1, so phi^(-4.5) < 1
  79    have h3 : phi ^ (-4.5 : ℝ) = 1 / (phi ^ (4.5 : ℝ)) := by
  80      rw [show (-4.5 : ℝ) = - (4.5 : ℝ) by norm_num]
  81      rw [Real.rpow_neg]
  82      · ring
  83      · exact le_of_lt phi_pos
  84    have h4 : phi ^ (4.5 : ℝ) > 1 := by
  85      -- Use the fact that phi > 1.618 > 1, so phi^4.5 > 1^4.5 = 1
  86      have hphi_gt : phi > (1.618 : ℝ) := by
  87        have h1 : phi > (1.618 : ℝ) := by
  88          have hsqrt5 : Real.sqrt 5 > (2.236 : ℝ) := by
  89            rw [show (2.236 : ℝ) = Real.sqrt (2.236^2) by rw [Real.sqrt_sq (by norm_num)]]
  90            apply Real.sqrt_lt_sqrt
  91            · norm_num
  92            · norm_num
  93          unfold phi
  94          linarith
  95        linarith
  96      have h1_pow : (1.618 : ℝ) ^ (4.5 : ℝ) > 1 := by
  97        -- 1.618^4.5 > 1 since 1.618 > 1
  98        have hbase : (1.618 : ℝ) > 1 := by norm_num
  99        have hexp_pos : (4.5 : ℝ) > 0 := by norm_num