structure
definition
T15Cert
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 90.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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
100
101end StrongForce
102end Physics
103end IndisputableMonolith