omega_lambda_positive

formal source

 114
 115    Since alphaInv > 2, alpha = 1/alphaInv < 1/2.
 116    And alpha/pi < alpha (since pi > 1) < 1/2 < 11/16. -/
 117theorem omega_lambda_positive : 11/16 - (alpha / Real.pi) > 0 := by
 118  have h_alphaInv_pos : alphaInv > 0 := by unfold alphaInv alpha_seed; positivity
 119  have h_alpha_pos : alpha > 0 := by unfold alpha; positivity
 120  -- alpha < 1/2 since alphaInv > 2
 121  have h_alpha_lt_half : alpha < 1/2 := by
 122    have h_eq : alpha = 1/alphaInv := by unfold alpha; field_simp
 123    rw [h_eq]
 124    rw [div_lt_div_iff₀ h_alphaInv_pos (by norm_num : (0:ℝ) < 2)]
 125    linarith [alphaInv_gt_2]
 126  -- alpha/pi < alpha (since pi > 1)
 127  have h_pi_gt_1 : Real.pi > 1 := by linarith [Real.pi_gt_three]
 128  have h_ratio : alpha / Real.pi < alpha := div_lt_self h_alpha_pos h_pi_gt_1
 129  linarith
 130
 131/-- **BOUNDS**: 0 < Ω_Λ < 11/16 -/
 132theorem omega_lambda_bounds : 0 < 11/16 - (alpha / Real.pi) ∧ 11/16 - (alpha / Real.pi) < 11/16 :=
 133  ⟨omega_lambda_positive, omega_lambda_lt_11_16⟩
 134
 135/-! ## Section P-002: Fermion Mass Hierarchy -/
 136
 137/-- **CALCULATED**: φ^6 bounds: 17 < φ^6 < 18.
 138    Uses φ^6 = (φ^3)^2 = (2φ+1)^2. -/
 139theorem phi_6_hierarchy_bounds : (17 : ℝ) < (phi : ℝ)^6 ∧ (phi : ℝ)^6 < (18 : ℝ) := by
 140  have h3 := phi_cubed_eq  -- phi^3 = 2*phi + 1
 141  have hphi_lo : phi > 1.61 := phi_gt_onePointSixOne
 142  have hphi_hi : phi < 1.62 := phi_lt_onePointSixTwo
 143  have h6 : phi^6 = (2 * phi + 1)^2 := by nlinarith [phi_pos]
 144  constructor
 145  · rw [h6]; nlinarith
 146  · rw [h6]; nlinarith
 147