sin2_theta_W
plain-language theorem explainer
Recognition Science sets the squared Weinberg angle to (3 - phi)/6 to relate W and Z masses on the electroweak phi-ladder. Boson mass verification certificates cite the definition to establish the wz_mass_ratio_sq equality and interval bounds near 0.2303. The declaration is a direct noncomputable assignment of the algebraic expression drawn from the imported phi constant.
Claim. $sin^2 theta_W = (3 - phi)/6$, where phi is the self-similar fixed point supplied by the Constants bundle.
background
The module treats electroweak boson masses via the formula m(EW, r) = 2 * phi^{50+r} / 10^6 MeV with B_pow = 1 and r0 = 55. The Weinberg angle supplies the link M_Z = M_W / cos(theta_W) between W and Z rungs on the phi-ladder. This definition supplies the RS-native value, separate from the experimental constant 0.23122 imported in ElectroweakBosons.
proof idea
The declaration is a direct definition that assigns the expression (3 - Constants.phi) / 6. No lemmas or tactics are applied; the body is the assignment itself.
why it matters
BosonVerificationCert depends on it to certify the bounds (0.2302, 0.2304) and the equality wz_mass_ratio_sq = cos2_theta_W. It also feeds cos2_theta_W and the electroweak results sin2_theta_approx and cos_theta_W. The definition completes the Weinberg angle step in the electroweak mass predictions, aligning the phi-ladder rung assignments with the observed weak-mixing value near 0.23.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.