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)
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
proof body
Term-mode proof.
247 simp only [runningMass]
248 field_simp
249
250/-! ## Anchor Relation -/
251
252/-- The anchor scale from the papers: μ⋆ = 182.201 GeV. -/
depends on (10)
Lean names referenced from this declaration's body.
-
gamma
in IndisputableMonolith.Constants.EulerMascheroni
decl_use
-
scale
in IndisputableMonolith.Cosmology.LargeScaleStructureFromRS
decl_use
-
from
in IndisputableMonolith.Foundation.PrimitiveDistinction
decl_use
-
Fermion
in IndisputableMonolith.Masses.RSBridge.Anchor
decl_use
-
Fermion
in IndisputableMonolith.Masses.SMVerification
decl_use
-
gamma
in IndisputableMonolith.NetworkScience.SmallWorldFromSigma
decl_use
-
AnomalousDimension
in IndisputableMonolith.Physics.RGTransport
decl_use
-
runningMass
in IndisputableMonolith.Physics.RGTransport
decl_use
-
gamma
in IndisputableMonolith.Relativity.ILG.PPN
decl_use
-
Fermion
in IndisputableMonolith.RSBridge.Anchor
decl_use