qcdParameterCount
plain-language theorem explainer
The declaration establishes that the inductive type enumerating the strong coupling and grouped quark masses has exactly five elements. Researchers certifying the RS-derived strong force parameters against PDG data cite this cardinality to confirm the count matches configDim D. The proof is a one-line wrapper applying the decide tactic to the derived Fintype instance.
Claim. The finite set of QCD parameters has cardinality five: $|QCDParameter| = 5$, where the elements are the strong coupling constant, the up/down quark masses, the strange quark mass, the charm/bottom quark masses, and the top quark mass.
background
In the module deriving the strong nuclear force from Recognition Science, QCDParameter is introduced as an inductive type whose five constructors group the strong coupling with quark mass sectors. This count is asserted to equal configDim D in the RS wallpaper-fraction derivation, where alpha_s(M_Z) = 2/17. The upstream result is the inductive definition of QCDParameter, which automatically derives the DecidableEq, Repr, BEq, and Fintype instances required for cardinality computation.
proof idea
The proof is a one-line wrapper that applies the decide tactic to the Fintype instance of QCDParameter.
why it matters
This supplies the five_params field inside the strongForceCert definition that certifies the RS strong coupling, its approximation band, and proximity to PDG values. It fills the parameter-count step in the module's derivation of alpha_s(M_Z) from the RS framework. In the broader chain it supports the connection between D = 3 and the five-parameter structure while leaving the explicit mass-ladder assignments for later results.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.