cos_sq_thetaW_in_unit_interval
plain-language theorem explainer
The theorem shows that cos²θ_W = g²/(g² + g'²) lies in (0,1] for any g > 0 and real g'. Electroweak model builders in the Recognition Science setting cite it to confirm the Weinberg angle stays admissible under the gauge-mass relations. The tactic proof unfolds the definition, invokes positivity on g² and the sum g² + g'², then applies div_pos and div_le_one.
Claim. For real numbers $g > 0$ and $g'$, define $c = g^2 / (g^2 + g'^2)$. Then $0 < c$ and $c ≤ 1$.
background
The ElectroweakMassBridge module encodes the tree-level SM relations m_W² = g² v² / 4 and m_Z² = (g² + g'²) v² / 4 together with the derived angle definitions cos²θ_W = g² / (g² + g'²) and sin²θ_W = g'² / (g² + g'²). These hold for any positive gauge couplings once the substrate scale v is supplied by HiggsEFTBridge. The present result guarantees that the cosine-squared quantity behaves as a valid fraction in (0,1].
proof idea
Unfold cos_sq_thetaW_SM. Positivity gives 0 < g² and 0 ≤ g'², so the denominator g² + g'² is positive. The lower bound is immediate from div_pos. The upper bound rewrites the claim as g² ≤ g² + g'² and applies div_le_one followed by linarith.
why it matters
The result is invoked inside electroweakMassBridgeCert to certify the full gauge-mass package. It supplies the unconditional gauge-relation half of the bridge, distinct from the RS-specific sin²θ_W = (3 − φ)/6 prediction in the companion ElectroweakMasses module. Within the framework it ensures the T7 eight-tick octave and D = 3 structure can host the electroweak sector without angle inconsistencies. The remaining open step is numerical calibration of g and g' from the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.