alpha_positive
open lean source
IndisputableMonolith.Unification.ConstantsPredictionsProved on GitHub at line 34.
browse module
All declarations in this module, on Recognition.
plain-language theorem explainer
The theorem establishes positivity of the fine-structure constant alpha derived from the geometric seed. Unification researchers cite it to confirm consistency of the alpha band before applying bounds or inflation certificates. The proof is a term-mode one-liner that unfolds the three definitions and applies the positivity tactic.
Claim. The fine-structure constant satisfies $0 < alpha$.
background
The ConstantsPredictionsProved module supplies calculated proofs for registry items including C-001 for the fine-structure constant. Alpha is defined as 1 over alphaInv where alphaInv equals alpha_seed times the exponential of minus f_gap over alpha_seed, and alpha_seed equals 4 pi times 11 from the geometric seed in Constants.Alpha. The module states that 0 < alpha < 0.1 is proved for this item.
proof idea
The term proof unfolds the definitions of alpha, alphaInv, and alpha_seed then applies the positivity tactic to conclude the result from the positive components of the expression.
why it matters
This result is used in alpha_bounds to establish 0 < alpha < 0.1, in constants_predictions_cert_exists, and inside the InflationCert structure for inflation_cert in Gravity.Inflation. It fills the C-001 entry in the COMPLETE_PROBLEM_REGISTRY and supports the alpha inverse band near 137 in the Recognition Science framework.
depends on
used by
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]