t15_verified
plain-language theorem explainer
The T15 certificate is assembled by pairing the exact derivation of the strong coupling constant from the count of wallpaper groups with its numerical agreement to PDG data. Researchers deriving coupling constants within the Recognition Science framework would cite this verified record. The definition directly instantiates the certificate structure using the two supporting theorems for geometric origin and experimental match.
Claim. The T15 certificate holds when the predicted strong coupling equals $2/17$ from the wallpaper group count and the absolute difference from the experimental value lies within the stated uncertainty.
background
In the Strong Force module the T15 proposition derives the strong coupling from the symmetry group count W=17. The structure T15Cert requires two fields: geometric_origin asserting that the prediction equals 2 divided by the number of wallpaper groups, and matches_pdg asserting that the absolute difference between prediction and experiment is less than the experimental error. The upstream theorem alpha_s_pred_eq_two_over_W establishes the exact equality to 2/17. The theorem alpha_s_match confirms that the absolute deviation 0.000253 is less than the PDG uncertainty 0.0009.
proof idea
The definition constructs the T15Cert record by assigning the geometric_origin field directly to the theorem alpha_s_pred_eq_two_over_W and the matches_pdg field to the theorem alpha_s_match. This is a direct structure instantiation with no additional computation.
why it matters
This declaration completes the formal verification of the T15 proposition for the strong force coupling as described in the module documentation. It records that the prediction 2/17 matches observation to within 0.2 sigma. Within the Recognition Science framework it parallels the derivation of the fine structure constant from edge geometry, here using the reciprocal of half the symmetry count. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.