theorem proved term proof

`mass_evo_exp_nf6`

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

formal statement (Lean)

 263theorem mass_evo_exp_nf6 : mass_evolution_exp 6 = 8 / 14 := by

proof body

Term-mode proof.

 264  unfold mass_evolution_exp mass_anomalous_dim b0_qcd; norm_num
 265
 266/-- LO QCD running mass at scale μ₂ given reference mass at μ₁.
 267    Uses real-valued power `rpow` since the exponent γ₀/(2b₀) is non-integer. -/

depends on (9)

Lean names referenced from this declaration's body.

scale in IndisputableMonolith.Cosmology.LargeScaleStructureFromRS decl_use
power in IndisputableMonolith.Cosmology.PrimordialSpectrum decl_use
is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
is in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi decl_use
is in IndisputableMonolith.GameTheory.MechanismDesignFromSigma decl_use
is in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use
b0_qcd in IndisputableMonolith.Physics.RunningCouplings decl_use
mass_anomalous_dim in IndisputableMonolith.Physics.RunningCouplings decl_use
mass_evolution_exp in IndisputableMonolith.Physics.RunningCouplings decl_use