pith. machine review for the scientific record. sign in
def definition def or abbrev

rg_residue_value

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  55def rg_residue_value (f : Fermion) (val : ℝ) : Prop :=

proof body

Definition body.

  56  -- This is a predicate stating that the species f has perturbative residue 'val'.
  57  True
  58
  59/-- The Recognition Strength for species f: the factor by which the geometric
  60    structure exceeds the perturbative RG effect. -/

depends on (10)

Lean names referenced from this declaration's body.