T15Cert
plain-language theorem explainer
The T15 certificate encodes the claim that the strong coupling equals twice the reciprocal of the seventeen wallpaper groups and lies inside the PDG experimental band. Physicists tracing gauge couplings to ledger symmetries would cite this structure to close the strong-force prediction. The certificate is assembled by direct substitution of the fixed group count into the prediction formula followed by a numerical bound check.
Claim. The T15 certificate asserts that the predicted strong coupling satisfies $alpha_s^{rm pred} = 2/W$ with $W=17$ the number of wallpaper groups, together with the bound $|alpha_s^{rm pred} - alpha_s^{rm exp}| < alpha_s^{rm err}$.
background
In the Recognition Science setting the strong coupling is obtained from the planar symmetries of the ledger, in contrast to the full edge geometry that yields the fine-structure constant. The module therefore sets the prediction to the reciprocal of half the wallpaper-group count, giving the numerical value 2/17. The constant wallpaper_groups is fixed at 17, the number of distinct two-dimensional wallpaper groups established by Fedorov in 1891; this count supplies the denominator of the curvature fraction and the geometric origin for the strong force. Upstream results supply the definition of wallpaper_groups as 17 together with the abbreviation W for that value.
proof idea
The structure T15Cert is introduced directly by its two fields. The geometric_origin field records the equality after casting wallpaper_groups to reals. The matches_pdg field records the absolute-difference bound. No tactics are applied; the certificate is populated downstream by explicit field assignment using the equality alpha_s_pred_eq_two_over_W and the match theorem alpha_s_match.
why it matters
This certificate supplies the verified instance of the T15 claim that the strong coupling arises from the wallpaper-group count in the ledger symmetries. It is consumed by the t15_verified definition that assembles the complete certificate. Within the forcing chain the result closes the geometric derivation of alpha_s, consistent with the eight-tick octave and the D=3 spatial dimensions already fixed upstream. No open scaffolding remains for this step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.