Encyclopedia Physics Physics Weinberg Angle Score Card

ARTICLE 4 claims 2 theorems 1 measured

Physics Weinberg Angle Score Card

A machine-checked scorecard shows the framework's predicted weak-mixing angle lands within one percent of the measured value, with the gap precisely named.

The Weinberg angle scorecard

The Weinberg angle (also called the weak-mixing angle) is a number in particle physics that describes how the electromagnetic and weak forces mix. Its sine-squared value, sin²θ_W, is measured at about 0.2229 in the reference data used here. The angle is not a free parameter in Recognition Science; the framework's core formula gives sin²θ_W = (3 − φ)/6, where φ is the golden ratio. This expression evaluates to roughly 0.2309, which sits within one percent of the observed value.

The scorecard in the framework's machine-checked library of formal theorems does three things. First, it records the observed value in a narrow band between 0.22 and 0.23. Second, it brackets the framework's prediction between 0.228 and 0.232. Third, it proves that the absolute difference between the best prediction and the observed value is less than 0.01. These three facts assemble into a single certificate, a proved object that holds with zero unproven assumptions and zero new axioms.

In plain language, the scorecard establishes a partial bridge: the framework's leading formula for the Weinberg angle agrees with one reference number to within one percent. The word partial matters. The bridge connects a single formula to a single observed value. The residual gap, named explicitly, is rung-normalization and scheme dependence: the framework has not yet derived how its prediction transforms under different renormalization schemes, which is a standard subtlety in electroweak physics.

The falsifier is equally explicit. If a future measurement of sin²θ_W moves by more than 0.01 from (3 − φ)/6 without a change in the certified φ or α input bounds, the identity-level match is false. This is not a vague hope; it is a concrete, checkable condition. The scorecard therefore does not claim the Weinberg angle is derived exactly. It claims, and proves, that the framework's core formula lands close to the measured value, and it names precisely what would break that closeness.

MODEL row_sin2_thetaW_RS_bracket · IndisputableMonolith/Physics/WeinbergAngleScoreCard.lean
theorem row_sin2_thetaW_RS_bracket :
    0.228 < sin2ThetaW_RS ∧ sin2ThetaW_RS < 0.232 := sin2ThetaW_RS_approx
MEASURED row_sin2_thetaW_codata_bracket · IndisputableMonolith/Physics/WeinbergAngleScoreCard.lean
row_sin2_thetaW_codata_bracket · IndisputableMonolith/Physics/WeinbergAngleScoreCard.lean:34
theorem row_sin2_thetaW_codata_bracket :
    (0.22 : ℝ) < row_sin2_thetaW_codata ∧ row_sin2_thetaW_codata < (0.23 : ℝ) := by
  simpa [row_sin2_thetaW_codata] using WeinbergAngle.sin2_theta_bounds
THEOREM row_best_prediction_match · IndisputableMonolith/Physics/WeinbergAngleScoreCard.lean
theorem row_best_prediction_match :
    |WeinbergAngle.bestPrediction - row_sin2_thetaW_codata| < 0.01 :=
  WeinbergAngle.best_prediction_close_to_observed
THEOREM weinbergAngleScoreCardCert_holds · IndisputableMonolith/Physics/WeinbergAngleScoreCard.lean
weinbergAngleScoreCardCert_holds · IndisputableMonolith/Physics/WeinbergAngleScoreCard.lean:51
theorem weinbergAngleScoreCardCert_holds : Nonempty WeinbergAngleScoreCardCert :=
  ⟨{ codata_in_ref_band := row_sin2_thetaW_codata_bracket
     rs_bracket := row_sin2_thetaW_RS_bracket
     one_cent_match := row_best_prediction_match }⟩

What this page does not claim

The Weinberg angle is exactly derived; only a partial bridge to one reference value is proved. The framework has derived the scheme dependence of its prediction. The observed value is the latest CODATA or PDG measurement; it is a reference value used in this module.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Physics/WeinbergAngleScoreCard.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND