sin2thetaW_pos
plain-language theorem explainer
The theorem proves that the Recognition Science expression for the sine squared of the weak mixing angle is strictly positive. Model builders deriving electroweak boson masses from the golden-ratio fixed point would cite it to confirm the parameter lies above zero. The proof is a short term-mode wrapper that unfolds the explicit fraction and combines a division-positivity lemma with the numerical bound on phi.
Claim. $0 < (3 - phi)/6$, where $phi$ is the golden-ratio fixed point of the Recognition Science forcing chain.
background
The Gauge Boson Masses from RS module supplies explicit formulas for Standard Model parameters obtained from the phi-ladder. It defines the weak mixing parameter as $(3 - phi)/6$ together with the mass ratio $m_Z/m_W = 6/(3 + phi)$. The module reports zero sorrys and zero axioms, indicating a complete formalization inside the Recognition Science setting.
proof idea
The proof unfolds the definition of the RS Weinberg parameter to the fraction $(3 - phi)/6$. It applies div_pos to reduce the claim to separate positivity of numerator and denominator, confirms the denominator is positive by norm_num, and invokes linarith together with the upstream lemma phi_lt_onePointSixTwo to establish that the numerator is positive.
why it matters
The result supplies the basic positivity check required for the RS-derived gauge-boson mass expressions to be physically admissible. It aligns with the self-similar fixed point phi obtained at steps T5-T6 of the unified forcing chain and supports further bounds such as the sin2thetaW band inside the same module. The construction rests on the Recognition Composition Law and the eight-tick octave that fix the mass-ladder spacing.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.