 234    `m(μ) = m(μ₀) · exp(-∫_{ln μ₀}^{ln μ} γ(μ') d(ln μ'))`
 235
 236    This is the solution to `d(ln m)/d(ln μ) = -γ_m(μ)`. -/
 237def runningMass (γ : AnomalousDimension) (f : Fermion) (m_μ₀ : ℝ) (lnμ₀ lnμ : ℝ) : ℝ :=
 238  m_μ₀ * Real.exp (-(∫ t in Set.Icc lnμ₀ lnμ, γ.gamma f (Real.exp t)))
 239
 240/-- The mass ratio between two scales.
 241
 242    `m(μ₁)/m(μ₀) = exp(-∫_{ln μ₀}^{ln μ₁} γ d(ln μ))` -/
 243theorem mass_ratio_formula (γ : AnomalousDimension) (f : Fermion) (m_μ₀ : ℝ)
 244    (lnμ₀ lnμ₁ : ℝ) (hm : m_μ₀ ≠ 0) :
 245    runningMass γ f m_μ₀ lnμ₀ lnμ₁ / m_μ₀ =
 246      Real.exp (-(∫ t in Set.Icc lnμ₀ lnμ₁, γ.gamma f (Real.exp t))) := by
 247  simp only [runningMass]
 248  field_simp
 249
 250/-! ## Anchor Relation -/
 251
 252/-- The anchor scale from the papers: μ⋆ = 182.201 GeV. -/
 253def muStar : ℝ := 182.201
 254
 255theorem muStar_pos : muStar > 0 := by norm_num [muStar]
 256
 257/-- ln(μ⋆) for use in integral bounds. -/
 258def lnMuStar : ℝ := Real.log muStar
 259
 260/-- The residue at the anchor, relative to a reference ln-scale.
 261
 262    `f_i(μ⋆, μ_ref) := (1/λ) ∫_{ln μ⋆}^{lnμ_ref} γ_i(exp(t)) dt`
 263
 264    This is what the axiom `f_residue` in `AnchorPolicy.lean` is intended to represent. -/
 265def residueAtAnchor (γ : AnomalousDimension) (f : Fermion) (lnμ_ref : ℝ) : ℝ :=
 266  integratedResidue γ f lnMuStar lnμ_ref
 267

papers checked against this theorem

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