No prose has been written for this declaration yet. The Lean source and graph data below render
without it.
generate prose now
formal statement (Lean)
190def implications : List String := [
proof body
Definition body.
191 "Electroweak mixing is fundamental, not arbitrary",
192 "The angle emerges from 8-tick geometry",
193 "Precise prediction possible with full RS model",
194 "Running coupling follows φ-ladder"
195]
196
197/-! ## Predictions and Tests -/
198
199/-- RS predictions for electroweak parameters:
200 1. sin²(θ_W) ~ 1/(2φ + 1) ≈ 0.236 (vs observed 0.223)
201 2. Running with energy follows φ-ladder
202 3. Mass ratio m_W/m_Z = cos(θ_W) ≈ 0.88 ✓ -/
depends on (14)
Lean names referenced from this declaration's body.
-
model
in IndisputableMonolith.ClassicalBridge.Fluids.CPM2D
decl_use
-
tick
in IndisputableMonolith.Constants
decl_use
-
Mass
in IndisputableMonolith.Constants.RSNativeUnits
decl_use
-
tick
in IndisputableMonolith.Constants.RSNativeUnits
decl_use
-
is
in IndisputableMonolith.Foundation.OptionAEmpiricalProgram
decl_use
-
from
in IndisputableMonolith.Foundation.PrimitiveDistinction
decl_use
-
is
in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi
decl_use
-
for
in IndisputableMonolith.Foundation.UniversalForcingSelfReference
decl_use
-
is
in IndisputableMonolith.GameTheory.MechanismDesignFromSigma
decl_use
-
is
in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom
decl_use
-
and
in IndisputableMonolith.NumberTheory.CirclePhaseLift
decl_use
-
emerges
in IndisputableMonolith.RecogGeom.Comparative
decl_use
-
m_W
in IndisputableMonolith.StandardModel.WZMassRatio
decl_use
-
m_Z
in IndisputableMonolith.StandardModel.WZMassRatio
decl_use