GaugeCouplingHierarchyScoreCardCert
plain-language theorem explainer
A certificate bundle packing seven gauge-hierarchy claims: α⁻¹_EM in (137.030, 137.039), 0 < sin²θ_W < 1, EM inverse coupling strictly above the weak one, gauge sum equal to 12π, α_s > 0, and zero free parameters. Anyone citing the RS three-coupling hierarchy scorecard uses this type. It is a pure structure definition; inhabitance is proved separately.
Claim. A certificate is a record of seven facts: the RS inverse fine-structure constant lies in $(137.030, 137.039)$; the RS weak mixing angle satisfies $0 < \sin^2\theta_W^{\mathrm{RS}} < 1$; $\alpha^{-1}_{\mathrm{EM}} > \alpha^{-1}_{\mathrm{weak}}$ where $\alpha^{-1}_{\mathrm{weak}} = \alpha^{-1}_{\mathrm{EM}}\sin^2\theta_W^{\mathrm{RS}}$; the predicted gauge sum equals $12\pi$; the predicted strong coupling is positive; and the free-parameter count is zero.
background
The module packages the Standard Model gauge hierarchy as forced by Recognition Science: electromagnetic, weak, and strong couplings with no free fits. The inverse fine-structure constant is the canonical RS expression (seed times exponential gap resummation), required to sit in the narrow band $(137.030, 137.039)$. The weak sector is tied in by $\sin^2\theta_W^{\mathrm{RS}} = (3-\varphi)/6$, and the inverse weak coupling is defined as $\alpha^{-1}{\mathrm{weak}} = \alpha^{-1}{\mathrm{EM}}\sin^2\theta_W^{\mathrm{RS}}$.
Strong coupling is the closed form $\alpha_s = \varphi^{-3}/\pi$. The gauge-sum prediction is $(\mathrm{cube_edges},3)\cdot\pi$, which evaluates to $12\pi$ in three spatial dimensions (T8). The scorecard also records that the free-parameter count on this hierarchy is identically zero. Upstream positivity of $\alpha_s$ is the elementary fact $\varphi^{-3}/\pi > 0$.
proof idea
No proof body: this is a structure whose fields are propositions. Each field name is a label for a Prop already established (or to be assembled) by sibling lemmas such as the EM band inequality, positivity and upper bound on $\sin^2\theta_W^{\mathrm{RS}}$, the EM-exceeds-weak comparison, the gauge-sum identity, $\alpha_s$ positivity, and the free-parameter count. Inhabitation is deferred to the companion theorem that builds a concrete record from those lemmas.
why it matters
This type is the single scorecard object for the three SM gauge couplings under RS forcing. The companion theorem gaugeCouplingHierarchyScoreCardCert_holds proves the structure is inhabited, wiring the band on $\alpha^{-1}$, the $\varphi$-derived weak angle, $\alpha_s = \varphi^{-3}/\pi$, and gauge sum $12\pi$ into one Nonempty certificate. That matches the module claim of zero free parameters and zero sorry.
Framework landmarks: T6 forces $\varphi$; T8 forces $D=3$, hence twelve cube edges and sum $12\pi$; the $\alpha^{-1}$ band is the RS infrared window cited in the primer. The structure does not close the OPEN infrared boundary-condition status of the exact CODATA $\alpha^{-1}(0)$; it only certifies the assembled RS expression lies in the stated open interval.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.