theorem proved term proof

`alpha_coupling_derived`

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

formal statement (Lean)

  80theorem alpha_coupling_derived : alpha > 0 := by

proof body

Term-mode proof.

  81  unfold alpha alphaInv alpha_seed
  82  positivity
  83
  84/-- **C-014.2**: Strong coupling α_s (at M_Z).
  85
  86    Derived from wallpaper groups: α_s = 2/17 ≈ 0.1176
  87    Matches PDG 2022: 0.1179 ± 0.0009
  88
  89    **Formula**: α_s = 2/W where W = 17 -/

depends on (10)

Lean names referenced from this declaration's body.

alpha in IndisputableMonolith.Constants.Alpha decl_use
alphaInv in IndisputableMonolith.Constants.Alpha decl_use
alpha_seed in IndisputableMonolith.Constants.Alpha decl_use
alpha_seed in IndisputableMonolith.Constants.AlphaHigherOrder decl_use
alpha_seed in IndisputableMonolith.Constants.AlphaPrecision decl_use
from in IndisputableMonolith.Foundation.PrimitiveDistinction decl_use
W in IndisputableMonolith.Masses.Anchor decl_use
W in IndisputableMonolith.Physics.LeptonGenerations.TauStepDerivation decl_use
W in IndisputableMonolith.Physics.MassTopology decl_use
Matches in IndisputableMonolith.RecogSpec.Core decl_use