rs_near_pdg
plain-language theorem explainer
Physicists deriving gauge couplings from the phi-ladder cite this result for the sub-percent agreement between (3 - φ)/6 and the measured sin²θ_W. The theorem shows the absolute difference to the PDG value 0.2312 is below 0.005. Its proof unfolds the two definitions, invokes abs_lt, and reduces both sides of the split inequality to the pre-proved band via linarith on the phi bounds.
Claim. $| (3 - φ)/6 - 0.2312 | < 0.005$
background
Recognition Science obtains the Weinberg angle from the rank decomposition of the gauge group. The prediction is sin²θ_W = (3 - φ)/6, with φ the golden ratio. The module fixes the PDG reference at 0.2312 and proves the RS value lies inside (0.228, 0.232) using the bounds 1.61 < φ < 1.62. Upstream, phi_gt_onePointSixOne and phi_lt_onePointSixTwo supply the tight interval for φ. The sin2thetaW_band theorem then translates these into the interval for sin²θ_W. The local setting is the A1 SM depth section, which links the formula to the (3,2,1) structure and reports 0.4% agreement with experiment.
proof idea
Unfold sin2thetaW and sin2thetaWPDG to expose (3 - φ)/6 and 0.2312. Rewrite the goal with abs_lt to obtain two inequalities. Introduce the phi bounds, then apply linarith to each half using the corresponding part of sin2thetaW_band.
why it matters
The declaration supplies the near_pdg field of sineSqThetaWCert, which packages the band and the PDG proximity. It realizes the claim from §XXIII.D that the phi-ladder formula matches PDG data to 0.4%. Within the framework this supports the gauge-boson spectrum derived from the eight-tick octave and the self-similar fixed point φ.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.