row_best_prediction_match
plain-language theorem explainer
The declaration shows that the Recognition Science prediction sin²θ_W = (3 - φ)/6 lies within 0.01 of the PDG-style observed value 0.2229. Electroweak precision physicists would cite it when checking φ-derived constants against measured mixing angles. The proof is a one-line wrapper that directly invokes the upstream closeness result best_prediction_close_to_observed.
Claim. $|(3 - φ)/6 - sin²θ_W^{obs}| < 0.01$
background
The module scorecard compares the RS core formula sin²θ_W = (3 - φ)/6 against the observed reference sin²θ_W ≈ 0.2229. row_sin2_thetaW_codata is defined as the observed value WeinbergAngle.sin2ThetaW_observed. bestPrediction is the noncomputable definition prediction3 that evaluates to (3 - φ)/6, with its doc-comment noting the ~3.2% error relative to 0.2229 and calling it the most promising φ-connection.
proof idea
One-line wrapper that applies the upstream theorem best_prediction_close_to_observed from the WeinbergAngle module.
why it matters
It supplies the one_cent_match field inside the constructor for weinbergAngleScoreCardCert_holds, completing the partial bridge between the RS prediction and codata. The module doc flags the residual open question of rung-normalization and scheme dependence. This sits inside the T5-T6 forcing chain that fixes φ as the self-similar point and feeds the alpha-band constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.