recognition / Constants / Constants.FermiConstantScoreCard / fermiConstantScoreCardCert_holds

theorem

`fermiConstantScoreCardCert_holds`

proved

show as: view math explainer →

module: IndisputableMonolith.Constants.FermiConstantScoreCard
domain: Constants
line: 110 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Constants.FermiConstantScoreCard on GitHub at line 110.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

Derivations using this theorem

Fermi Coupling Constant Inside CODATA Bracket · derived / THEOREM
The weak coupling G_F * (mu c)^2 / (hbar c)^3 lands inside the RS certified bracket

depends on

formal source

 107    (1.16e-5 : ℝ) < row_fermi_codata ∧ row_fermi_codata < (1.17e-5 : ℝ)
 108  vev_range : (244 : ℝ) < vev_canonical ∧ vev_canonical < (248 : ℝ)
 109
 110theorem fermiConstantScoreCardCert_holds :
 111    Nonempty FermiConstantScoreCardCert :=
 112  ⟨{ fermi_bracket := row_fermi_pred_bracket
 113     codata_in_bracket := row_fermi_codata_in_bracket
 114     vev_range := vev_in_range }⟩
 115
 116end
 117
 118end IndisputableMonolith.Constants.FermiConstantScoreCard

papers checked against this theorem

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