`two_div_17_upper`

proved

show as: view math explainer →

module: IndisputableMonolith.Physics.StrongForce
domain: Physics
line: 69 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Physics.StrongForce on GitHub at line 69.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

  66  simp only [alpha_s_geom]
  67  norm_num
  68
  69theorem two_div_17_upper : (alpha_s_geom : ℝ) < 0.118 := by
  70  simp only [alpha_s_geom]
  71  norm_num
  72
  73/-- The predicted value is within experimental error of the measured value.
  74
  75    pred = 2/17 ≈ 0.117647...
  76    exp  = 0.1179
  77    err  = 0.0009
  78
  79    |pred - exp| = |0.117647 - 0.1179| = 0.000253 < 0.0009 ✓
  80
  81    This is now PROVEN, not axiomatized. -/
  82theorem alpha_s_match :
  83    abs (alpha_s_pred - alpha_s_exp) < alpha_s_err := by
  84  simp only [alpha_s_pred, alpha_s_geom, alpha_s_exp, alpha_s_err]
  85  norm_num
  86
  87/-! ## Certificate -/
  88
  89/-- T15 Certificate: Strong coupling derived from wallpaper groups. -/
  90structure T15Cert where
  91  /-- The prediction is 2/W with W=17 wallpaper groups. -/
  92  geometric_origin : alpha_s_pred = 2 / (wallpaper_groups : ℝ)
  93  /-- The prediction matches experiment within uncertainty. -/
  94  matches_pdg : abs (alpha_s_pred - alpha_s_exp) < alpha_s_err
  95
  96/-- The T15 certificate is verified. -/
  97def t15_verified : T15Cert where
  98  geometric_origin := alpha_s_pred_eq_two_over_W
  99  matches_pdg := alpha_s_match

papers checked against this theorem

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