theorem proved term proof

`alpha_high_precision`

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

formal statement (Lean)

  26theorem alpha_high_precision (h : H_AlphaPrecision) :
  27    ∃ (error : ℝ), abs (alphaInv - 137.035999) < error ∧ error < 1e-11 := h

Term-mode proof.

  28
  29end Alpha
  30end Physics
  31end IndisputableMonolith

Lean names referenced from this declaration's body.

alphaInv in IndisputableMonolith.Constants.Alpha decl_use
H_AlphaPrecision in IndisputableMonolith.Physics.AlphaHighPrecision decl_use