`Fermion`

definition

show as: view math explainer →

module: IndisputableMonolith.Masses.RSBridge.Anchor
domain: Masses
line: 34 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Masses.RSBridge.Anchor on GitHub at line 34.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  31inductive Sector | up | down | lepton | neutrino
  32deriving DecidableEq, Repr
  33
  34inductive Fermion
  35| d | s | b | u | c | t | e | mu | tau | nu1 | nu2 | nu3
  36deriving DecidableEq, Repr, Inhabited
  37
  38def sectorOf : Fermion → Sector
  39| .d | .s | .b => .down
  40| .u | .c | .t => .up
  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**:

papers checked against this theorem

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