structure
definition
StrongCouplingCert
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Constants.StrongCoupling on GitHub at line 65.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
62
63/-! ## Certificate -/
64
65structure StrongCouplingCert where
66 positive : 0 < alpha_s_prediction
67 gauge_structure : gauge_sum_prediction = 12 * Real.pi
68 gauge_bounded : (36 : ℝ) < gauge_sum_prediction ∧ gauge_sum_prediction < 48
69
70theorem strong_coupling_cert_exists : Nonempty StrongCouplingCert :=
71 ⟨{ positive := alpha_s_positive
72 gauge_structure := gauge_sum_value
73 gauge_bounded := gauge_sum_bounds }⟩
74
75end
76
77end IndisputableMonolith.Constants.StrongCoupling