sin2ThetaW_alt
plain-language theorem explainer
This definition supplies an alternative expression for the square of the Weinberg angle in terms of the golden ratio. A researcher deriving electroweak parameters inside Recognition Science would cite it when testing φ-constrained mixing. The definition is obtained by direct substitution of the self-similar fixed point into the angle formula.
Claim. $sin^2 θ_W := (φ - 1)/(2φ)$, where φ denotes the golden ratio.
background
The module targets derivation of the W/Z mass ratio from Recognition Science's φ-structure. Observed masses give m_W/m_Z ≈ 0.8815, which equals cos θ_W by definition, while the measured sin²(θ_W) sits near 0.223. Recognition Science posits that the electroweak mixing angle is fixed by φ-quantized gauge structure, with φ the unique positive solution to φ = 1 + 1/φ.
proof idea
The declaration is a direct definition that equates the alternative expression to (φ - 1) divided by twice φ. No lemmas or tactics are invoked beyond the arithmetic identity for the golden ratio.
why it matters
The definition contributes to the module's goal of obtaining electroweak parameters from φ-forcing. It aligns with the chain step that identifies φ as the self-similar fixed point and supports the claim that unification follows from the recognizer structure. The module flags a numerical mismatch (formula yields ≈0.191) and notes potential for a PRL paper on RS-derived predictions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.