theorem proved term proof

`lambda_qcd_scale`

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

formal statement (Lean)

 154theorem lambda_qcd_scale : 100 < lambda_QCD ∧ lambda_QCD < 300 := by

proof body

Term-mode proof.

 155  unfold lambda_QCD
 156  constructor <;> norm_num
 157
 158/-! ## Dimensional Transmutation -/
 159
 160/-- Dimensional transmutation: a dimensionless coupling g generates
 161    a mass scale Λ through running. The proton mass m_p ~ Λ_QCD
 162    emerges from the gauge coupling through RG evolution. -/

depends on (5)

Lean names referenced from this declaration's body.

scale in IndisputableMonolith.Cosmology.LargeScaleStructureFromRS decl_use
from in IndisputableMonolith.Foundation.PrimitiveDistinction decl_use
lambda_QCD in IndisputableMonolith.QFT.RunningCouplings decl_use
emerges in IndisputableMonolith.RecogGeom.Comparative decl_use
m_p in IndisputableMonolith.StandardModel.ProtonMass decl_use