lambda_qcd_scale
plain-language theorem explainer
lambda_qcd_scale establishes that the QCD scale parameter satisfies 100 < Lambda_QCD < 300 in MeV units. Phenomenologists matching Recognition Science outputs to hadron data would cite this numerical anchor. The proof is a one-line wrapper that unfolds the constant definition to 200 and applies norm_num to verify both sides of the interval.
Claim. $100 < Lambda_{QCD} < 300$ (in MeV).
background
The QFT module derives running couplings from phi-ladder scaling, where distinct rungs label energy scales and J-cost optimization varies with rung. Lambda_QCD is introduced as the noncomputable constant 200 MeV that sets the strong-interaction mass scale generated by dimensional transmutation. Upstream results supply the scale function phi^k from cosmology and the proton-mass definition that links this scale to observable hadron masses; the primitive-distinction theorem supplies the axiomatic base for the overall framework.
proof idea
The term proof unfolds the definition of lambda_QCD, splits the conjunction with constructor, and invokes norm_num on each inequality to confirm the numerical bounds hold for the constant 200.
why it matters
The result supplies the order-of-magnitude claim required by the dimensional-transmutation paragraph in the QFT module and anchors the QCD scale for downstream proton-mass and large-scale-structure calculations. It realizes the RS mechanism in which phi-ladder rungs determine energy scales, consistent with the eight-tick octave and D=3 geometry. It leaves open the derivation of the precise numerical value directly from the phi-ladder rather than as an input constant.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.