module module

`IndisputableMonolith.StandardModel.WeinbergAngle`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

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