structure
definition
StrongCouplingCert
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
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