alpha_positive

formal source

  31/-! ## Section C-001: Fine-Structure Constant α -/
  32
  33/-- **CALCULATED**: α > 0 (fine-structure constant is positive). -/
  34theorem alpha_positive : alpha > 0 := by
  35  unfold alpha alphaInv alpha_seed
  36  positivity
  37
  38/-- **CALCULATED**: α < 0.1 (approximately 1/137 < 0.1). -/
  39theorem alpha_lt_0_1 : alpha < (0.1 : ℝ) := by
  40  -- Use alphaInv > 10 from structural bound
  41  -- alphaInv ≥ alpha_seed - f_gap > 132 - 5 = 127 > 10
  42  have h_seed_pos : alpha_seed > 0 := by unfold alpha_seed; positivity
  43  have h_seed_big : alpha_seed > 132 := by unfold alpha_seed; nlinarith [Real.pi_gt_three]
  44  have h_exp_ge : Real.exp (-(f_gap / alpha_seed)) ≥ 1 - f_gap / alpha_seed := by
  45    have := Real.add_one_le_exp (-(f_gap / alpha_seed)); linarith
  46  -- f_gap < 5 < alpha_seed - 10 (since alpha_seed > 132)
  47  have h_fgap_small : f_gap < alpha_seed - 10 := by
  48    -- Same structure as in RegistryPredictionsProved
  49    -- w8 < 5 and log(phi) < 1, so f_gap < 5 < 122 < alpha_seed - 10
  50    have h_w8_pos : 0 < w8_from_eight_tick := w8_pos
  51    have h_log_lt1 : Real.log phi < 1 := by
  52      rw [← Real.log_exp 1]
  53      apply Real.log_lt_log phi_pos
  54      linarith [Real.add_one_le_exp (1 : ℝ), phi_lt_onePointSixTwo]
  55    have h_fgap_lt_w8 : f_gap < w8_from_eight_tick := by
  56      unfold f_gap
  57      calc w8_from_eight_tick * Real.log phi
  58          < w8_from_eight_tick * 1 := mul_lt_mul_of_pos_left h_log_lt1 h_w8_pos
  59        _ = w8_from_eight_tick := mul_one _
  60    have h_sqrt2_lo : Real.sqrt 2 > 1.4 := by
  61      rw [show (1.4:ℝ) = Real.sqrt (1.4^2) from (Real.sqrt_sq (by norm_num : (0:ℝ) ≤ 1.4)).symm]
  62      exact Real.sqrt_lt_sqrt (by norm_num) (by norm_num)
  63    have h_sqrt2_hi : Real.sqrt 2 < 1.42 := by
  64      rw [show (1.42:ℝ) = Real.sqrt (1.42^2) from (Real.sqrt_sq (by norm_num : (0:ℝ) ≤ 1.42)).symm]