StrongForceCert
plain-language theorem explainer
The StrongForceCert structure packages four independent facts: the RS strong coupling equals exactly 2/17, lies inside the open interval (0.117, 0.119), differs from the PDG reference 0.118 by less than 0.001, and the QCDParameter inductive type has cardinality five. A physicist checking RS-derived Standard Model inputs would cite this certificate to record the alpha_s(M_Z) match. The declaration is a plain structure definition that merely assembles the four properties from already-defined constants.
Claim. Let $a_s = 2/17$. The certificate asserts $a_s = 2/17$, $0.117 < a_s < 0.119$, $|a_s - 0.118| < 0.001$, and that the inductive type enumerating the five QCD quantities (strong coupling, up/down masses, strange mass, charm/bottom masses, top mass) has exactly five constructors.
background
The module derives the strong nuclear force from Recognition Science by identifying the strong coupling with the rational 2/17 obtained from the wallpaper-fraction construction. The inductive type QCDParameter lists the five quantities alphaSStrong, massUd, massSStrange, massCB and massTop, and carries a Fintype instance so that its cardinality is well-defined. The constant alphaSPDG supplies the PDG reference value 0.118. This local setting follows the RS derivation in which five parameters match the configuration dimension D.
proof idea
The declaration is a structure definition with no proof body. Each field is filled directly from the sibling definitions: strongCouplingRS supplies the equality and the numerical band, alphaSPDG supplies the PDG comparison, and the Fintype instance on QCDParameter supplies the cardinality statement.
why it matters
StrongForceCert records the numerical success of the RS prediction for alpha_s(M_Z) and is instantiated by the downstream definition strongForceCert. The result sits inside the broader Recognition Science program that obtains all constants from the J-uniqueness functional equation and the phi fixed point; here the five-parameter count is tied to the configuration dimension D. No open scaffolding remains in this file.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.