`row_fermi_pred`

definition

show as: view math explainer →

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

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Constants.FermiConstantScoreCard on GitHub at line 50.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  47/-! ## Re-exported row aliases -/
  48
  49/-- P1-C01 Fermi constant prediction in GeV^-2 natural units. -/
  50noncomputable def row_fermi_pred : ℝ :=
  51  1 / (Real.sqrt 2 * vev_canonical ^ 2)
  52
  53/-- CODATA/PDG Fermi constant in GeV^-2. -/
  54def row_fermi_codata : ℝ := 1.1663787e-5
  55
  56theorem row_fermi_pred_eq :
  57    row_fermi_pred = 1 / (Real.sqrt 2 * vev_canonical ^ 2) := rfl
  58
  59private theorem sqrt2_pos : 0 < Real.sqrt 2 := Real.sqrt_pos.mpr (by norm_num)
  60
  61private theorem fermi_den_pos : 0 < Real.sqrt 2 * vev_canonical ^ 2 := by
  62  have hv : 0 < vev_canonical ^ 2 := sq_pos_of_ne_zero (ne_of_gt vev_canonical_pos)
  63  nlinarith [sqrt2_pos, hv]
  64
  65theorem row_fermi_pred_lower :
  66    (1.16e-5 : ℝ) < row_fermi_pred := by
  67  unfold row_fermi_pred
  68  rw [lt_div_iff₀ fermi_den_pos]
  69  have hs : Real.sqrt 2 < (1.4143 : ℝ) := sqrt2_lt_14143
  70  have hden :
  71      Real.sqrt 2 * vev_canonical ^ 2 < (1.4143 : ℝ) * (246 : ℝ) ^ 2 := by
  72    have hv : vev_canonical = (246 : ℝ) := rfl
  73    have hvpos : 0 < vev_canonical ^ 2 := sq_pos_of_ne_zero (ne_of_gt vev_canonical_pos)
  74    rw [hv]
  75    nlinarith
  76  have hnum : (1.16e-5 : ℝ) * ((1.4143 : ℝ) * (246 : ℝ) ^ 2) < 1 := by
  77    norm_num
  78  nlinarith
  79
  80theorem row_fermi_pred_upper :

papers checked against this theorem

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