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)
131theorem row_muon_pct :
132 |Verification.rs_mass_MeV .Lepton 13 - Verification.m_mu_exp| /
133 Verification.m_mu_exp < 0.04 :=
proof body
Term-mode proof.
134 Verification.muon_relative_error
135
136/-- Tau mass within 3 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
-
m_mu_exp
in IndisputableMonolith.Masses.Verification
decl_use
-
muon_relative_error
in IndisputableMonolith.Masses.Verification
decl_use
-
rs_mass_MeV
in IndisputableMonolith.Masses.Verification
decl_use
-
Lepton
in IndisputableMonolith.Physics.AnomalousMoments
decl_use