def definition def or abbrev

`mass_match`

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

formal statement (Lean)

  54def mass_match (mass_above alpha_at_threshold : ℝ) : ℝ :=

proof body

Definition body.

  55  mass_above * (1 + d_2_mass * (alpha_at_threshold / Real.pi) ^ 2)
  56
  57/-! ## Positivity of matching factors
  58
  59For the small alpha values that occur at the heavy-quark thresholds
  60(alpha_s(m_b) ~ 0.22, alpha_s(m_c) ~ 0.38), the corrections are at the
  61percent level and never threaten positivity. We prove this conditionally
  62on the input being positive and the alpha being below 1 (perturbative). -/
  63

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

mass_match_pos in IndisputableMonolith.Physics.QCDRGE.ThresholdMatching decl_use
ThresholdMatchingCert in IndisputableMonolith.Physics.QCDRGE.ThresholdMatching decl_use

depends on (9)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
alpha in IndisputableMonolith.Constants.Alpha decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
and in IndisputableMonolith.NumberTheory.CirclePhaseLift decl_use
that in IndisputableMonolith.NumberTheory.PhiLadderLattice decl_use
d_2_mass in IndisputableMonolith.Physics.QCDRGE.ThresholdMatching decl_use