StrongCouplingCert
plain-language theorem explainer
The StrongCouplingCert structure packages three properties of the RS gauge predictions: positivity of alpha_s = phi^{-3}/pi, exact equality of the three-gauge sum to 12 pi, and the interval 36 < sum < 48. A unification-scale physicist would cite it when checking consistency of the phi-derived couplings against the eight-tick structure. The definition is a direct record constructor with no lemmas or reductions.
Claim. A certificate consists of a proof that the predicted strong coupling satisfies $0 < phi^{-3}/pi$, an equality asserting that the gauge sum equals $12 pi$, and bounds $36 <$ gauge sum $< 48$.
background
Module StrongCoupling derives the strong coupling from the 8-tick gauge structure of Recognition Science. The three gauge couplings at unification are fixed by cube geometry: alpha_EM from 44 pi resummation, alpha_weak from sin^2 theta_W = (3-phi)/6, and alpha_s from the remaining degrees of freedom. Upstream, alpha_s_prediction is defined as phi^{-3}/pi and gauge_sum_prediction as (cube_edges 3) * pi, which evaluates to 12 pi.
proof idea
The declaration is a structure definition whose three fields directly record the required properties. No tactics, lemmas, or reductions are applied; the fields reference the sibling definitions alpha_s_positive, gauge_sum_value, and gauge_sum_bounds.
why it matters
The certificate is the witness used by strong_coupling_cert_exists to establish Nonempty StrongCouplingCert. It closes the Q9 question on deriving alpha_s(M_Z) from the RS phi-geometry and eight-tick octave (T7). The bounds interval supplies a concrete check against the PDG central value 0.118.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.