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)
125theorem row_electron_pct :
126 |Verification.rs_mass_MeV .Lepton 2 - Verification.m_e_exp| /
127 Verification.m_e_exp < 0.003 :=
proof body
Term-mode proof.
128 Verification.electron_relative_error
129
130/-- Muon mass within 4 percent of PDG. -/
used by (2)
From the project-wide theorem graph. These declarations reference this one in their body.
depends on (10)
Lean names referenced from this declaration's body.
-
of
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
decl_use
-
Lepton
in IndisputableMonolith.CrossDomain.CubeFaceUniversality
decl_use
-
of
in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization
decl_use
-
of
in IndisputableMonolith.Foundation.PhiForcingDerived
decl_use
-
of
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
of
in IndisputableMonolith.Information.PhysicsComplexityStructure
decl_use
-
electron_relative_error
in IndisputableMonolith.Masses.Verification
decl_use
-
m_e_exp
in IndisputableMonolith.Masses.Verification
decl_use
-
rs_mass_MeV
in IndisputableMonolith.Masses.Verification
decl_use
-
Lepton
in IndisputableMonolith.Physics.AnomalousMoments
decl_use