module module high

`IndisputableMonolith.StandardModel.WeinbergAngle`

This module registers definitions and bounds for sin²(θ_W) at the Z-pole in the MS-bar scheme within the Recognition Science Standard Model. Electroweak and unification researchers cite it when comparing the RS-native value (3-φ)/6 against PDG-style data. The module itself is a registry of constants and sibling predictions with no internal proofs.

claim$sin^2 θ_W$ at the Z mass in the MS-bar scheme, with observed reference ≈0.2229 and RS prediction (3-φ)/6.

background

The module sits in the StandardModel domain and imports the RS time quantum τ₀ = 1 tick from Constants. It defines the electroweak mixing angle together with observed value, error, bounds, and five numbered predictions plus a bestPrediction, all tied to the eight-tick geometry and geometricMixing. The local setting uses the J-uniqueness and phi fixed point to generate gauge parameters without re-deriving the forcing chain.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

Supplies the electroweak parameter registry required by WeinbergAngleScoreCard (which states the RS core sin²θ_W = (3-φ)/6 and observed ≈0.2229), GaugeCouplingsComplete (C-014 on gauge couplings from RS structure), and HiggsRungAssignment (phi-ladder mass table). It closes the registry step for the T7 eight-tick octave applied to mixing angles.

scope and limits

Does not derive (3-φ)/6 from the forcing chain inside this file.
Does not propagate experimental errors beyond listed bounds.
Does not address scale dependence or running of the angle.
Does not contain the geometricMixing proof itself.

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