tildeQ

formal source

  41| .e | .mu | .tau => .lepton
  42| .nu1 | .nu2 | .nu3 => .neutrino
  43
  44def tildeQ : Fermion → ℤ
  45| .u | .c | .t => 4
  46| .d | .s | .b => -2
  47| .e | .mu | .tau => -6
  48| .nu1 | .nu2 | .nu3 => 0
  49
  50def ZOf (f : Fermion) : ℤ :=
  51  let q := tildeQ f
  52  match sectorOf f with
  53  | .up | .down => 4 + q*q + q*q*q*q
  54  | .lepton     =>     q*q + q*q*q*q
  55  | .neutrino   => 0
  56
  57/-- The display function F(Z) = ln(1 + Z/φ) / ln(φ).
  58
  59    This is the **closed form** that the integrated RG residue is claimed to equal
  60    at the anchor scale μ⋆. The claim is:
  61      `f_i(μ⋆) = gap(ZOf i)`
  62    where `f_i(μ⋆)` is the integral of the mass anomalous dimension.
  63
  64    **Properties**:
  65    - F(0) = 0
  66    - F is monotonically increasing for Z > -φ
  67    - For large Z: F(Z) ≈ log_φ(Z)
  68
  69    **Canonical values** (charged fermions):
  70    - F(24)   ≈ 5.74   (down quarks, q̃ = -2)
  71    - F(276)  ≈ 10.69  (up quarks, q̃ = +4)
  72    - F(1332) ≈ 13.95  (leptons, q̃ = -6) -/
  73noncomputable def gap (Z : ℤ) : ℝ :=
  74  (Real.log (1 + (Z : ℝ) / (Constants.phi))) / (Real.log (Constants.phi))