theorem
proved
two_div_17_lower
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Physics.StrongForce on GitHub at line 65.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
62/-! ## Verification -/
63
64/-- Helper: 2/17 bounds using direct computation. -/
65theorem two_div_17_lower : (0.117 : ℝ) < (alpha_s_geom : ℝ) := by
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