IndisputableMonolith.Constants.FermiConstantScoreCard

   1import Mathlib
   2import IndisputableMonolith.Constants.ElectroweakVEVStructure
   3import IndisputableMonolith.Numerics.Interval.W8Bounds
   4
   5/-!
   6# Fermi Constant Score Card
   7
   8Phase 1 row **P1-C01** in `planning/PHYSICAL_DERIVATION_PLAN.md`.
   9
  10## Statement
  11
  12The theorem-grade slice is the natural-unit electroweak identity
  13
  14`G_F = 1 / (sqrt 2 * v^2)`
  15
  16with the canonical RS electroweak VEV surface `v = 246 GeV`.
  17
  18## Measurement target
  19
  20CODATA / PDG:
  21
  22`G_F = 1.1663787 x 10^-5 GeV^-2`.
  23
  24This module proves the interval
  25
  26`1.16 x 10^-5 < G_F^RS < 1.17 x 10^-5`,
  27
  28so the CODATA value sits inside the bracket. The row remains
  29**PARTIAL_THEOREM** because `ElectroweakVEVStructure.vev_canonical = 246`
  30is the canonical GeV display value; the fully derived SI/GeV VEV bridge
  31is still open.
  32
  33Falsifier: CODATA/PDG `G_F` outside `(1.16e-5, 1.17e-5) GeV^-2`, or a
  34future VEV bridge that does not recover the canonical 246 GeV scale.
  35
  36## Lean status: 0 sorry, 0 axiom
  37-/
  38
  39namespace IndisputableMonolith.Constants.FermiConstantScoreCard
  40
  41open IndisputableMonolith.Constants.ElectroweakVEVStructure
  42open IndisputableMonolith.Numerics
  43open IndisputableMonolith.Numerics.W8Bounds
  44
  45noncomputable section
  46
  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 :
  81    row_fermi_pred < (1.17e-5 : ℝ) := by
  82  unfold row_fermi_pred
  83  rw [div_lt_iff₀ fermi_den_pos]
  84  have hs : (1.4142 : ℝ) < Real.sqrt 2 := sqrt2_gt_14142
  85  have hden :
  86      (1.4142 : ℝ) * (246 : ℝ) ^ 2 < Real.sqrt 2 * vev_canonical ^ 2 := by
  87    have hv : vev_canonical = (246 : ℝ) := rfl
  88    rw [hv]
  89    nlinarith
  90  have hnum : 1 < (1.17e-5 : ℝ) * ((1.4142 : ℝ) * (246 : ℝ) ^ 2) := by
  91    norm_num
  92  nlinarith
  93
  94theorem row_fermi_pred_bracket :
  95    (1.16e-5 : ℝ) < row_fermi_pred ∧ row_fermi_pred < (1.17e-5 : ℝ) :=
  96  ⟨row_fermi_pred_lower, row_fermi_pred_upper⟩
  97
  98theorem row_fermi_codata_in_bracket :
  99    (1.16e-5 : ℝ) < row_fermi_codata ∧ row_fermi_codata < (1.17e-5 : ℝ) := by
 100  unfold row_fermi_codata
 101  constructor <;> norm_num
 102
 103structure FermiConstantScoreCardCert where
 104  fermi_bracket :
 105    (1.16e-5 : ℝ) < row_fermi_pred ∧ row_fermi_pred < (1.17e-5 : ℝ)
 106  codata_in_bracket :
 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
 119