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)
79theorem tau_pred_eq : rs_mass_MeV .Lepton 19 = tau_pred :=
proof body
Term-mode proof.
80 lepton_pred_eq_aux 76 19 (by norm_num)
81
82/-! ## Phi-Power Transfer Lemmas -/
83
used by (2)
From the project-wide theorem graph. These declarations reference this one in their body.
depends on (8)
Lean names referenced from this declaration's body.
-
Phi
in IndisputableMonolith.Cost.AczelProof
decl_use
-
Phi
in IndisputableMonolith.Cost.AczelTheorem
decl_use
-
Lepton
in IndisputableMonolith.CrossDomain.CubeFaceUniversality
decl_use
-
lepton_pred_eq_aux
in IndisputableMonolith.Masses.Verification
decl_use
-
rs_mass_MeV
in IndisputableMonolith.Masses.Verification
decl_use
-
tau_pred
in IndisputableMonolith.Masses.Verification
decl_use
-
Lepton
in IndisputableMonolith.Physics.AnomalousMoments
decl_use
-
Power
in IndisputableMonolith.Superhuman.Core
decl_use