IndisputableMonolith.Masses.QuarkAnchorDerivation

   1import Mathlib
   2import IndisputableMonolith.Masses.RSBridge.Anchor
   3
   4/-!
   5# Heavy Quark Anchor Derivation
   6
   7This module derives the heavy-quark anchor-scale masses directly from the
   8RSBridge formula
   9
  10  `massAtAnchor f = M0 * exp(((rung f : ℝ) - 8 + gap (ZOf f)) * log φ)`.
  11
  12No PDG masses enter. The result is RS-native and dimensionless.
  13-/
  14
  15namespace IndisputableMonolith.Masses.QuarkAnchorDerivation
  16
  17open IndisputableMonolith.RSBridge
  18
  19noncomputable section
  20
  21def charm_anchor_native : ℝ := massAtAnchor Fermion.c
  22def bottom_anchor_native : ℝ := massAtAnchor Fermion.b
  23def top_anchor_native : ℝ := massAtAnchor Fermion.t
  24
  25theorem charm_anchor_eq_massAtAnchor :
  26    charm_anchor_native = massAtAnchor Fermion.c := rfl
  27
  28theorem bottom_anchor_eq_massAtAnchor :
  29    bottom_anchor_native = massAtAnchor Fermion.b := rfl
  30
  31theorem top_anchor_eq_massAtAnchor :
  32    top_anchor_native = massAtAnchor Fermion.t := rfl
  33
  34theorem charm_rung_eq : rung Fermion.c = 15 := rfl
  35theorem bottom_rung_eq : rung Fermion.b = 21 := rfl
  36theorem top_rung_eq : rung Fermion.t = 21 := rfl
  37
  38theorem charm_Z_eq : ZOf Fermion.c = 276 := rfl
  39theorem bottom_Z_eq : ZOf Fermion.b = 24 := rfl
  40theorem top_Z_eq : ZOf Fermion.t = 276 := rfl
  41
  42theorem heavy_anchor_positive :
  43    0 < charm_anchor_native ∧
  44    0 < bottom_anchor_native ∧
  45    0 < top_anchor_native := by
  46  unfold charm_anchor_native bottom_anchor_native top_anchor_native massAtAnchor
  47  constructor
  48  · exact mul_pos M0_pos (Real.exp_pos _)
  49  constructor
  50  · exact mul_pos M0_pos (Real.exp_pos _)
  51  · exact mul_pos M0_pos (Real.exp_pos _)
  52
  53structure QuarkAnchorDerivationCert where
  54  charm_rung : rung Fermion.c = 15
  55  bottom_rung : rung Fermion.b = 21
  56  top_rung : rung Fermion.t = 21
  57  charm_Z : ZOf Fermion.c = 276
  58  bottom_Z : ZOf Fermion.b = 24
  59  top_Z : ZOf Fermion.t = 276
  60  positive : 0 < charm_anchor_native ∧
  61    0 < bottom_anchor_native ∧
  62    0 < top_anchor_native
  63
  64theorem quarkAnchorDerivationCert_holds : QuarkAnchorDerivationCert :=
  65{ charm_rung := charm_rung_eq
  66  bottom_rung := bottom_rung_eq
  67  top_rung := top_rung_eq
  68  charm_Z := charm_Z_eq
  69  bottom_Z := bottom_Z_eq
  70  top_Z := top_Z_eq
  71  positive := heavy_anchor_positive }
  72
  73end
  74
  75end IndisputableMonolith.Masses.QuarkAnchorDerivation
  76