sin2_theta_W_rs
plain-language theorem explainer
The declaration supplies the Recognition Science zero-parameter prediction for sin²θ_W as (3 − φ)/6. Electroweak mass derivations cite it to obtain m_W from m_Z via the gauge relation without adjustable inputs. The definition is a direct algebraic assignment drawn from the Constants bundle.
Claim. $sin^2 θ_W = (3 - φ)/6$ where φ is the golden ratio.
background
The ElectroweakMasses module fixes the Z boson at rung 1 on the phi-ladder, giving m_Z = 2 φ^51 / 10^6 MeV, then derives m_W = m_Z cos θ_W. The local setting distinguishes this from the earlier undifferentiated r_boson placeholder by introducing the Weinberg angle through the RS-native expression for sin²θ_W. The module imports the Constants structure from LawOfExistence, an abstract bundle holding Knet, Cproj, Ceng, Cdisp together with the nonnegativity condition on Knet.
proof idea
The definition is a direct noncomputable assignment of the real number (3 - Constants.phi) / 6. No lemmas or tactics are invoked; the expression serves as the primitive input for all downstream identities.
why it matters
This supplies the zero-parameter input for the electroweak sector and feeds directly into cos2_theta_W_rs, alpha_W, sin2_theta_positive, and sin2_theta_lt_half. It realizes the module's stated differentiation of W and Z masses and sits inside the forcing chain through the golden-ratio fixed point and the eight-tick octave. The parent results are the electroweak coupling definitions in WeakCoupling.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.