strongForceCert
plain-language theorem explainer
The definition assembles a certificate asserting that the RS-derived strong coupling equals exactly 2/17, lies inside the open interval (0.117, 0.119), differs from the PDG value by less than 0.001, and that QCD involves precisely five parameters. A researcher deriving Standard Model couplings from the Recognition Science forcing chain would cite this to certify the strong sector. The construction is a direct structure instantiation that pulls each field from an upstream numerical or decidable result.
Claim. Let $a_s^{RS}$ denote the RS strong coupling at the $Z$ scale. The certificate asserts $a_s^{RS} = 2/17$, $0.117 < a_s^{RS} < 0.119$, $|a_s^{RS} - a_s^{PDG}| < 0.001$, and that the set of QCD parameters has cardinality 5.
background
In this module the strong coupling is obtained from the Recognition Science wallpaper-fraction rule, yielding the exact rational 2/17. The certificate structure collects four independent properties: the equality to 2/17, a numerical band around the predicted value 0.1176, proximity to the experimental PDG figure, and the count of five QCD parameters (corresponding to the three colors together with the configuration dimension $D=3$ of the underlying phi-ladder). Upstream results supply each property separately: one by reflexivity on the rational expression, one by direct numerical bounds, one by a norm_num comparison to the PDG datum, and one by a decidable cardinality check on the finite type of QCD parameters.
proof idea
The definition is a direct structure constructor that assigns the four fields of the certificate from the four upstream results. The equality field is taken from the reflexivity theorem on the rational 2/17. The band field is taken from the norm_num verification of the open interval. The near-PDG field is taken from the norm_num distance computation. The parameter-count field is taken from the decide tactic on the finite cardinality.
why it matters
The certificate certifies the strong-force sector of the Recognition Science derivation, confirming that the predicted value 2/17 lies inside the PDG tolerance and that the parameter count matches the expected configuration dimension. It thereby anchors the strong coupling inside the same framework that produces the electromagnetic fine-structure constant inside (137.030, 137.039) and the eight-tick octave. No downstream theorems yet consume the certificate, leaving open its later use in a full Standard-Model certification theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.