module module high

`IndisputableMonolith.StandardModel.WeinbergAngle`

The module records the observed sin²θ_W at the Z mass in the MS-bar scheme together with five RS predictions and an EightTickGeometry mixing construction. Electroweak unification researchers cite it when benchmarking the Recognition Science phi-ladder against PDG data. The module is a pure collection of definitions and numerical bounds with no theorems.

claimDefines the reference value $sin^2 θ_W^{obs} ≈ 0.2229$ (MS-bar at $m_Z$), the interval bounds, the RS core prediction $sin^2 θ_W = (3-φ)/6$, and the geometric mixing map arising from the eight-tick octave.

background

Recognition Science obtains the Weinberg angle from the Q3 geometry and the eight-tick period (T7). The module imports the base time quantum τ₀ = 1 tick from Constants. It introduces the observed reference sin2ThetaW_observed, the error sin2ThetaW_error, the interval sin2_theta_bounds, five explicit prediction terms, the bestPrediction selector, and the geometricMixing function that encodes the eight-tick mixing.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

Supplies the numerical anchor and geometricMixing construction required by the WeinbergAngleScoreCard (P2-θW phase) and by GaugeCouplingsComplete. The downstream scorecard directly compares the RS value (3-φ)/6 against the observed 0.2229 reference recorded here.

scope and limits

Does not derive sin²θ_W from the forcing chain; it only records the reference value.
Does not compute renormalization-group evolution of the angle.
Does not include higher-order electroweak radiative corrections.
Does not address the running of sin²θ_W to other energy scales.

used by (3)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Physics.WeinbergAngleScoreCard module_import
IndisputableMonolith.StandardModel.HiggsRungAssignment module_import
IndisputableMonolith.Unification.GaugeCouplingsComplete module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import

declarations in this module (23)

def sin2ThetaW_observed L39
def sin2ThetaW_error L42
theorem sin2_theta_bounds L45
def prediction1 L57
def prediction2 L64
def prediction3 L71
def prediction4 L78
def prediction5 L85
def bestPrediction L94
theorem best_prediction_close_to_observed L96
structure EightTickGeometry L117
def geometricMixing L126
theorem simple_geometric_ratio L132
def phiCorrection L144
def correctedPrediction L146
def sin2ThetaW_GUT L158
theorem gut_prediction L161
def runningAngle L169
def deepConnections L181
structure ExperimentalMeasurement L200
def measurements L205
structure WeinbergAngleFalsifier L217
def derivationStatus L226