sin2_theta_bounds
plain-language theorem explainer
The declaration proves the observed sin squared theta W at the Z mass scale lies strictly between 0.22 and 0.23. An electroweak phenomenologist comparing Recognition Science predictions to data would cite this numeric bracket. The proof is a one-line wrapper that unfolds the constant definition and applies numeric normalization to confirm both sides of the conjunction.
Claim. $0.22 < s < 0.23$ where $s$ is the observed value of $sin^2 theta_W$ at the Z-boson mass scale in the MS-bar scheme.
background
Module SM-004 targets derivation of the weak mixing angle theta_W from RS phi-structure, with the angle fixing the relative strengths of electromagnetic and weak forces. The observed value is supplied by the upstream definition sin2ThetaW_observed : R := 0.2229. This bound anchors comparison against the module's phi-based predictions such as 1/4 - 1/(8 phi) which evaluates near 0.1727.
proof idea
The proof unfolds sin2ThetaW_observed to expose the literal value 0.2229. Constructor splits the conjunction into two goals; norm_num then verifies each inequality by direct numeric reduction.
why it matters
The result supplies the observed bracket consumed by the downstream theorem row_sin2_thetaW_codata_bracket in Physics.WeinbergAngleScoreCard, which applies it via simpa. It anchors the five phi-derived predictions listed in the module against data, consistent with the paper proposition on Electroweak Mixing from Information-Theoretic Principles and the eight-tick phase geometry of the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.