theorem proved term proof

`alpha_s_geom_eq`

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

formal statement (Lean)

  58theorem alpha_s_geom_eq : (alpha_s_geom : ℝ) = 2 / 17 := by

Term-mode proof.

  59  simp only [alpha_s_geom]
  60  norm_num
  61
  62/-! ## Verification -/
  63
  64/-- Helper: 2/17 bounds using direct computation. -/

Lean names referenced from this declaration's body.