weinbergAngleScoreCardCert_holds
plain-language theorem explainer
The theorem shows that the scorecard certificate structure for the Weinberg angle is inhabited, confirming that the Recognition Science prediction for sin²θ_W lies inside a 0.01 window of the codata reference while both sit inside their stated numerical brackets. Electroweak precision physicists would cite it as a concrete numerical check of the phi-derived formula against PDG-style data. The proof is a direct term construction that packages three sibling lemmas into the required structure fields.
Claim. The scorecard certificate structure is inhabited: there exist bounds such that $0.22 < s < 0.23$, $0.228 < sin^2θ_W^{RS} < 0.232$, and $|bestPrediction - s| < 0.01$, where $s$ denotes the codata reference value for $sin^2θ_W$ and $bestPrediction$ is the RS-derived estimate.
background
The module implements Phase 2 of the Recognition Science electroweak scorecard. Its core prediction is $sin^2θ_W = (3-φ)/6$, taken from the Q3Representations module, while the observed reference is the PDG-style value $sin^2θ_W ≈ 0.2229$. The certificate structure packages three concrete numerical claims: the codata reference lies in (0.22, 0.23), the RS value lies in (0.228, 0.232), and their absolute difference is less than 0.01. The module doc states that this constitutes a proved partial bridge whose residual issues are rung normalization and scheme dependence.
proof idea
The term proof directly constructs the certificate record by supplying the three required fields. It uses row_sin2_thetaW_codata_bracket for the codata interval, row_sin2_thetaW_RS_bracket for the RS interval, and row_best_prediction_match for the one-cent closeness condition. Each of those lemmas is itself a one-line wrapper around an upstream bound or approximation lemma.
why it matters
This declaration supplies the top-level existence witness for the Weinberg angle scorecard, completing the Phase 2 P2-θW bridge inside the Recognition Science forcing chain. It directly instantiates the partial numerical match described in the module doc between the phi-based formula and experimental codata. Because the used-by list is empty, the result functions as a terminal certification object for this module; any larger electroweak unification argument would import it to close the sin²θ_W check. The open residual named in the module doc is scheme dependence after rung normalization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.