pith. machine review for the scientific record. sign in
theorem proved tactic proof

alpha_lower_bound

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  97theorem alpha_lower_bound : (0.00729 : ℝ) < Constants.alpha := by

proof body

Tactic-mode proof.

  98  -- From the rigorous interval proof: alphaInv < 137.039 ⇒ 1/137.039 < alpha
  99  have h_inv_lt : Constants.alphaInv < (137.039 : ℝ) := by
 100    simpa [Constants.alphaInv] using (IndisputableMonolith.Numerics.alphaInv_lt)
 101  have h_inv_pos : (0 : ℝ) < Constants.alphaInv := by
 102    have h := IndisputableMonolith.Numerics.alphaInv_gt
 103    linarith
 104  -- Invert inequality (antitone on positive reals).
 105  have h_one_div : (1 / (137.039 : ℝ)) < 1 / Constants.alphaInv := by
 106    exact one_div_lt_one_div_of_lt h_inv_pos h_inv_lt
 107  -- Translate to alpha = 1/alphaInv and weaken the numeric constant to 0.00729.
 108  have h_num : (0.00729 : ℝ) < (1 / (137.039 : ℝ)) := by norm_num
 109  simpa [Constants.alpha, one_div] using lt_trans h_num h_one_div
 110

used by (7)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (9)

Lean names referenced from this declaration's body.