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)
111noncomputable def massRatio : ℝ := phi
proof body
Definition body.
112
113/-- Approximate mass ratios in the Standard Model:
114 - top/charm ≈ 130 ≈ φ^10
115 - charm/up ≈ 500 ≈ φ^13
116 - tau/muon ≈ 17 ≈ φ^6
117 - muon/electron ≈ 207 ≈ φ^11
118
119 The pattern is φ^n for various n. -/
used by (13)
From the project-wide theorem graph. These declarations reference this one in their body.
-
GaugeBosonMassCert
in IndisputableMonolith.Physics.GaugeBosonMassesFromRS
decl_use
-
massRatio
in IndisputableMonolith.Physics.GaugeBosonMassesFromRS
decl_use
-
massRatio_gt_one
in IndisputableMonolith.Physics.GaugeBosonMassesFromRS
decl_use
-
massRatio_pos
in IndisputableMonolith.Physics.GaugeBosonMassesFromRS
decl_use
-
row_WZ_ratio_bracket
in IndisputableMonolith.Physics.WZBosonRatioScoreCard
decl_use
-
WZBosonRatioScoreCardCert
in IndisputableMonolith.Physics.WZBosonRatioScoreCard
decl_use
-
massRatio
in IndisputableMonolith.StandardModel.NeutrinoMassHierarchy
decl_use
-
mass_ratio_phi7
in IndisputableMonolith.StandardModel.NeutrinoMassHierarchy
decl_use
-
massRatio
in IndisputableMonolith.StandardModel.WZMassRatio
decl_use
-
mass_ratio_value
in IndisputableMonolith.StandardModel.WZMassRatio
decl_use
-
sin2ThetaW
in IndisputableMonolith.StandardModel.WZMassRatio
decl_use
-
sin2_theta_w_value
in IndisputableMonolith.StandardModel.WZMassRatio
decl_use
-
weinbergAngle
in IndisputableMonolith.StandardModel.WZMassRatio
decl_use
depends on (10)
Lean names referenced from this declaration's body.
-
Model
in IndisputableMonolith.CPM.LawOfExistence
decl_use
-
is
in IndisputableMonolith.Foundation.OptionAEmpiricalProgram
decl_use
-
is
in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi
decl_use
-
for
in IndisputableMonolith.Foundation.UniversalForcingSelfReference
decl_use
-
is
in IndisputableMonolith.GameTheory.MechanismDesignFromSigma
decl_use
-
tau
in IndisputableMonolith.Masses.Anchor
decl_use
-
is
in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom
decl_use
-
massRatio
in IndisputableMonolith.Physics.GaugeBosonMassesFromRS
decl_use
-
massRatio
in IndisputableMonolith.StandardModel.NeutrinoMassHierarchy
decl_use
-
massRatio
in IndisputableMonolith.StandardModel.WZMassRatio
decl_use