WeinbergAngleScoreCardCert
plain-language theorem explainer
The structure certifies that the Recognition Science prediction for sin²θ_W agrees with the observed datum to within 0.01 while both quantities lie inside stated intervals. An electroweak phenomenologist would cite the certificate when tabulating phi-derived parameters against reference data. The structure is assembled by embedding three pre-proved interval facts supplied by sibling definitions.
Claim. A structure certifying that the observed value $s$ of $sin^2 theta_W$ satisfies $0.22 < s < 0.23$, the RS value $(3-phi)/6$ satisfies $0.228 < (3-phi)/6 < 0.232$, and the absolute difference between the best RS prediction and $s$ is less than 0.01.
background
The module records a scorecard for the Weinberg angle inside the Recognition Science treatment of the electroweak sector. The RS core prediction is the closed expression $(3-phi)/6$ drawn from the Q3 representation; the observed reference is the fixed real near 0.2229 imported from standard data. The structure simply packages the three interval statements that document a 1 percent numerical agreement between these two quantities.
proof idea
The declaration is a structure definition whose fields are three independent real-number inequalities. Each field is discharged by direct reference to a sibling definition that has already established the bound; no further reduction or tactic is applied.
why it matters
The structure supplies the certificate object whose non-emptiness is asserted by the downstream theorem weinbergAngleScoreCardCert_holds. It implements the partial bridge described in the module header for Phase 2, linking the phi-derived formula to experimental sin²θ_W. The match is consistent with the Recognition Science program that obtains electroweak parameters from the J-cost functional and the phi fixed point; scheme dependence remains the named residual.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.