IndisputableMonolith.Physics.GaugeCouplingHierarchyScoreCard
Scorecard module for the RS gauge-coupling hierarchy: Weinberg angle, inverse weak and EM couplings, the EM band, a 12π sum identity, strong-coupling positivity, and a zero-free-parameter certificate. Physicists checking whether RS fixes the SM gauge sector without knobs cite it. Content is mostly closed-form defs plus short positivity and band lemmas wired into one cert.
claimRS gauge hierarchy scorecard: $\sin^2\theta_W$ from the RS closed form (with $0<\sin^2\theta_W<1$), inverse weak coupling, EM exceeding weak, $\alpha^{-1}_{\mathrm{em}}$ inside the RS band, the gauge sum identity involving $12\pi$, $\alpha_s>0$, and a certificate that the hierarchy uses zero free parameters.
background
Recognition Science fixes gauge data from $\varphi$-geometry and the eight-tick structure rather than fitting couplings. Upstream, Constants supplies the RS-native tick and base constants; StrongCoupling asks whether $\alpha_s(M_Z)$ is forced by $\varphi$-geometry (Q9); AlphaBounds gives rigorous interval bounds on $\alpha^{-1}$ from the symbolic derivation; W8Bounds pins the gap weight $w_8$ from the eight-tick closed form $w_8=(348+210\sqrt{2}-(204+130\sqrt{2})\varphi)/7\approx 2.490569$.
This module assembles those pieces into hierarchy statements: an RS value for $\sin^2\theta_W$, derived inverse weak coupling, comparison of EM to weak, the EM inverse-coupling band, a $12\pi$ gauge-sum relation, positivity of $\alpha_s$, and an explicit free-parameter count forced to zero. The local setting is a physics scorecard, not a derivation of the full SM Lagrangian.
proof idea
Definition-heavy scorecard with short supporting lemmas. Closed forms introduce $\sin^2\theta_W$ and the inverse weak coupling; positivity and unit-interval bounds are elementary inequalities on those forms. EM-vs-weak and the $\alpha^{-1}$ band reuse the interval machinery from AlphaBounds. The $12\pi$ sum and $\alpha_s>0$ are direct algebraic or sign checks against StrongCoupling and W8 data. free_params / zero_free_params count adjustable inputs and discharge them. The top cert GaugeCouplingHierarchyScoreCardCert packages the conjunction; gaugeCouplingHierarchyScoreCardCert_holds is the one-shot proof that the package is inhabited.
why it matters in Recognition Science
Places the RS claim that the gauge hierarchy (Weinberg angle, relative EM/weak strength, $\alpha^{-1}$ band, strong coupling) is parameter-free on a single auditable card. It sits downstream of the $\varphi$-forced constants, the $\alpha^{-1}$ interval work, the eight-tick $w_8$ weight, and the strong-coupling Q9 line, and packages them for physics-side review. No further in-repo used_by edges are recorded; the module is a terminal scorecard rather than a lemma feeder. Landmark contact: T6 $\varphi$ fixed point, T7 eight-tick octave (via $w_8$), and the RS $\alpha^{-1}$ band near $(137.030,137.039)$.
scope and limits
- Does not derive the full electroweak Lagrangian or Higgs sector.
- Does not prove running of couplings beyond the stated band and positivity facts.
- Does not claim experimental fit quality outside the cited $\alpha^{-1}$ interval.
- Does not introduce new forcing-chain steps T0–T8; it consumes constants from them.
- Does not bound neutrino or Yukawa sectors.
depends on (4)
declarations in this module (12)
-
def
sin2_W_rs -
theorem
sin2_W_pos -
theorem
sin2_W_lt_one -
def
alpha_weak_inv -
theorem
em_exceeds_weak -
theorem
alpha_inv_em_band -
theorem
gauge_sum_12pi -
theorem
alpha_s_pos -
def
free_params -
theorem
zero_free_params -
structure
GaugeCouplingHierarchyScoreCardCert -
theorem
gaugeCouplingHierarchyScoreCardCert_holds