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)
181def deepConnections : List String := [
proof body
Definition body.
182 "Charge quantization from discrete phases",
183 "Mass ratio from φ-constrained symmetry breaking",
184 "Unification from φ-ladder convergence"
185]
186
187/-! ## Experimental Tests -/
188
189/-- The Weinberg angle is one of the most precisely measured quantities in physics.
190
191 | Measurement | Value | Error |
192 |-------------|-------|-------|
193 | LEP (Z pole) | 0.2312 | 0.0002 |
194 | SLD (asymmetries) | 0.2310 | 0.0002 |
195 | Moller scattering | 0.2403 | 0.0013 |
196 | νN DIS | 0.2277 | 0.0016 |
197 | APV (Cs) | 0.2356 | 0.0020 |
198
199 The variation with energy ("running") is also measured. -/
depends on (22)
Lean names referenced from this declaration's body.
-
of
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
decl_use
-
Charge
in IndisputableMonolith.Constants.RSNativeUnits
decl_use
-
Mass
in IndisputableMonolith.Constants.RSNativeUnits
decl_use
-
Measurement
in IndisputableMonolith.Data.Import
decl_use
-
of
in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization
decl_use
-
one
in IndisputableMonolith.Foundation.IntegersFromLogic
decl_use
-
is
in IndisputableMonolith.Foundation.OptionAEmpiricalProgram
decl_use
-
of
in IndisputableMonolith.Foundation.PhiForcingDerived
decl_use
-
from
in IndisputableMonolith.Foundation.PrimitiveDistinction
decl_use
-
one
in IndisputableMonolith.Foundation.RationalsFromLogic
decl_use
-
is
in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi
decl_use
-
of
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
is
in IndisputableMonolith.GameTheory.MechanismDesignFromSigma
decl_use
-
of
in IndisputableMonolith.Information.PhysicsComplexityStructure
decl_use
-
quantization
in IndisputableMonolith.LedgerUnits
decl_use
-
Z
in IndisputableMonolith.Masses.Anchor
decl_use
-
is
in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom
decl_use
-
Measurement
in IndisputableMonolith.Measurement.RSNative.Core
decl_use
-
Z
in IndisputableMonolith.Physics.AnchorPolicyCertified
decl_use
-
one
in IndisputableMonolith.QFT.SpinStatistics
decl_use
-
Measurement
in IndisputableMonolith.Quantum.NonlocalityNoSignaling
decl_use
-
one
in IndisputableMonolith.RecogSpec.Core
decl_use