recognition / Constants / Constants.StrongCoupling / strong_coupling_cert_exists

theorem

`strong_coupling_cert_exists`

proved

show as: view math explainer →

module: IndisputableMonolith.Constants.StrongCoupling
domain: Constants
line: 70 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Constants.StrongCoupling on GitHub at line 70.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

Derivations using this theorem

Strong Coupling alpha_s from the Gauge Sum · derived / THEOREM
alpha_s is forced by the RS gauge-sum prediction and its bounds

depends on

formal source

  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

papers checked against this theorem

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