deficit_bounded

formal source

  52
  53/-- **THEOREM EA-003.2**: The deficit is bounded (not catastrophic).
  54    Ratio > 0.70 means ~30% max deficit. -/
  55theorem deficit_bounded : ga_capture_ratio > 0.70 := by
  56  unfold ga_capture_ratio ga_capture_measured ga_capture_predicted
  57  norm_num
  58
  59/-! ## II. The φ-Ladder Structure -/
  60
  61/-- Gallium rung on the φ-ladder (from mass ~70 u). -/
  62noncomputable def gallium_rung : ℕ := 45
  63
  64/-- The φ-suppression factor for Ga. -/
  65noncomputable def phi_suppression_ga : ℝ := phi ^ (-(gallium_rung : ℝ) / 10)
  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