predicted_mass_tau — Recognition explainer

formal statement (Lean)

  63noncomputable def predicted_mass_tau : ℝ :=

proof body

Definition body.

  64  electron_structural_mass * phi ^ predicted_residue_tau
  65
  66end LeptonGenerations
  67end Physics
  68end IndisputableMonolith

used by (24)

From the project-wide theorem graph. These declarations reference this one in their body.

muon_mass_step_hypothesis in IndisputableMonolith.Physics.LeptonGenerations decl_use
tau_mass_pred_bounds in IndisputableMonolith.Physics.LeptonGenerations decl_use
tau_mass_step_hypothesis in IndisputableMonolith.Physics.LeptonGenerations decl_use
lepton_ladder_forced_from_T9 in IndisputableMonolith.Physics.LeptonGenerations.Necessity decl_use
lepton_ladder_forced_from_T9_v2 in IndisputableMonolith.Physics.LeptonGenerations.Necessity decl_use
muon_mass_pred_bounds_tight in IndisputableMonolith.Physics.LeptonGenerations.Necessity decl_use
predicted_mass_tau_lower in IndisputableMonolith.Physics.LeptonGenerations.Necessity decl_use
predicted_mass_tau_lower_tight in IndisputableMonolith.Physics.LeptonGenerations.Necessity decl_use
predicted_mass_tau_lower_v2 in IndisputableMonolith.Physics.LeptonGenerations.Necessity decl_use
predicted_mass_tau_upper in IndisputableMonolith.Physics.LeptonGenerations.Necessity decl_use
predicted_mass_tau_upper_tight in IndisputableMonolith.Physics.LeptonGenerations.Necessity decl_use
predicted_mass_tau_upper_v2 in IndisputableMonolith.Physics.LeptonGenerations.Necessity decl_use
tau_mass_pred_bounds_proven in IndisputableMonolith.Physics.LeptonGenerations.Necessity decl_use
tau_mass_pred_bounds_tight in IndisputableMonolith.Physics.LeptonGenerations.Necessity decl_use
tau_mass_pred_bounds_v2 in IndisputableMonolith.Physics.LeptonGenerations.Necessity decl_use
muon_mass_step_hypothesis in IndisputableMonolith.RRF.Physics.LeptonGenerations decl_use
tau_mass_pred_bounds in IndisputableMonolith.RRF.Physics.LeptonGenerations decl_use
tau_mass_step_hypothesis in IndisputableMonolith.RRF.Physics.LeptonGenerations decl_use
predicted_mass_tau in IndisputableMonolith.RRF.Physics.LeptonGenerations.Defs decl_use
lepton_ladder_forced_from_T9 in IndisputableMonolith.RRF.Physics.LeptonGenerations.Necessity decl_use
muon_mass_pred_bounds_proven in IndisputableMonolith.RRF.Physics.LeptonGenerations.Necessity decl_use
predicted_mass_tau_lower in IndisputableMonolith.RRF.Physics.LeptonGenerations.Necessity decl_use
predicted_mass_tau_upper in IndisputableMonolith.RRF.Physics.LeptonGenerations.Necessity decl_use
tau_mass_pred_bounds_proven in IndisputableMonolith.RRF.Physics.LeptonGenerations.Necessity decl_use

depends on (5)

Lean names referenced from this declaration's body.

electron_structural_mass in IndisputableMonolith.Physics.ElectronMass.Defs decl_use
predicted_residue_tau in IndisputableMonolith.Physics.LeptonGenerations.Defs decl_use
electron_structural_mass in IndisputableMonolith.RRF.Physics.ElectronMass.Defs decl_use
predicted_mass_tau in IndisputableMonolith.RRF.Physics.LeptonGenerations.Defs decl_use
predicted_residue_tau in IndisputableMonolith.RRF.Physics.LeptonGenerations.Defs decl_use