QCDParameter
plain-language theorem explainer
The QCDParameter inductive type enumerates the five QCD inputs in the RS derivation of the strong force: strong coupling, up/down masses, strange mass, charm/bottom masses, and top mass. Researchers working on the alpha_s(M_Z) = 2/17 prediction cite it when counting parameters or building certification structures. It is supplied directly as an inductive definition that derives DecidableEq, Repr, BEq, and Fintype with no further obligations.
Claim. Let the set of QCD parameters be the inductive type whose five constructors are the strong coupling constant, the combined up and down quark masses, the strange quark mass, the combined charm and bottom quark masses, and the top quark mass.
background
In the Strong Nuclear Force from RS module the Recognition Science derivation begins from the wallpaper-fraction identity that fixes alpha_s(M_Z) = 2/17. The module states that exactly five QCD parameters are required and that this number equals the configuration dimension. The parameters are grouped as alpha_s, u/d masses, s mass, c/b masses, and top mass. The file imports Mathlib for type-class support and Constants for the surrounding RS units.
proof idea
The declaration is a plain inductive definition with five constructors. It derives the four type classes DecidableEq, Repr, BEq, and Fintype automatically. No lemmas or tactics are applied.
why it matters
QCDParameter supplies the enumeration used by qcdParameterCount to establish cardinality five and by StrongForceCert to certify the coupling lies inside the PDG band while satisfying the five-parameter count. It realizes the module claim that five parameters match configDim D and anchors the RS prediction alpha_s = 2/17 inside the forcing-chain framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.