`alphaSPDG`

definition

show as: view math explainer →

module: IndisputableMonolith.Physics.StrongNuclearForceFromRS
domain: Physics
line: 33 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Physics.StrongNuclearForceFromRS on GitHub at line 33.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

used by

formal source

  30  unfold strongCouplingRS; norm_num
  31
  32/-- PDG α_s(M_Z) = 0.118 is within 0.001 of RS. -/
  33def alphaSPDG : ℝ := 0.118
  34theorem alphaSRS_near_PDG : |(strongCouplingRS : ℝ) - alphaSPDG| < 0.001 := by
  35  unfold alphaSPDG strongCouplingRS
  36  norm_num
  37
  38inductive QCDParameter where
  39  | alphaSStrong | massUd | massSStrange | massCB | massTop
  40  deriving DecidableEq, Repr, BEq, Fintype
  41
  42theorem qcdParameterCount : Fintype.card QCDParameter = 5 := by decide
  43
  44structure StrongForceCert where
  45  coupling_eq : strongCouplingRS = 2 / 17
  46  coupling_band : (strongCouplingRS : ℝ) > 0.117 ∧ (strongCouplingRS : ℝ) < 0.119
  47  near_pdg : |(strongCouplingRS : ℝ) - alphaSPDG| < 0.001
  48  five_params : Fintype.card QCDParameter = 5
  49
  50def strongForceCert : StrongForceCert where
  51  coupling_eq := strongCouplingRS_eq
  52  coupling_band := strongCoupling_approx
  53  near_pdg := alphaSRS_near_PDG
  54  five_params := qcdParameterCount
  55
  56end IndisputableMonolith.Physics.StrongNuclearForceFromRS

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.