theorem proved term proof

`mass_evolution_exp_pos`

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

formal statement (Lean)

 250theorem mass_evolution_exp_pos (n_f : ℕ) (h : n_f ≤ 16) :
 251    0 < mass_evolution_exp n_f := by

proof body

Term-mode proof.

 252  unfold mass_evolution_exp
 253  exact div_pos mass_anomalous_dim_pos
 254    (mul_pos (by norm_num) (asymptotic_freedom_criterion n_f h))
 255
 256/-- Concrete mass evolution exponents for physical n_f values. -/

depends on (4)

Lean names referenced from this declaration's body.

for in IndisputableMonolith.Foundation.UniversalForcingSelfReference decl_use
asymptotic_freedom_criterion in IndisputableMonolith.Physics.RunningCouplings decl_use
mass_anomalous_dim_pos in IndisputableMonolith.Physics.RunningCouplings decl_use
mass_evolution_exp in IndisputableMonolith.Physics.RunningCouplings decl_use