def
definition
predicted_mass_mu
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Physics.LeptonGenerations.Defs on GitHub at line 59.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
-
Mass -
electron_structural_mass -
predicted_residue_mu -
electron_structural_mass -
predicted_mass_mu -
predicted_residue_mu
used by
-
muon_mass_pred_bounds -
muon_mass_step_hypothesis -
lepton_ladder_forced_from_T9 -
lepton_ladder_forced_from_T9_v2 -
muon_mass_pred_bounds_proven -
muon_mass_pred_bounds_tight -
muon_mass_pred_bounds_v2 -
phi_pow_residue_tau_bounds -
predicted_mass_mu_lower -
predicted_mass_mu_lower_tight -
predicted_mass_mu_lower_v2 -
predicted_mass_mu_upper -
predicted_mass_mu_upper_tight -
predicted_mass_mu_upper_v2 -
muon_mass_pred_bounds -
muon_mass_step_hypothesis -
predicted_mass_mu -
lepton_ladder_forced_from_T9 -
muon_mass_pred_bounds_proven -
phi_pow_residue_tau_bounds -
predicted_mass_mu_lower -
predicted_mass_mu_upper
formal source
56/-! ## Mass Predictions -/
57
58/-- Predicted Muon Mass. -/
59noncomputable def predicted_mass_mu : ℝ :=
60 electron_structural_mass * phi ^ predicted_residue_mu
61
62/-- Predicted Tau Mass. -/
63noncomputable def predicted_mass_tau : ℝ :=
64 electron_structural_mass * phi ^ predicted_residue_tau
65
66end LeptonGenerations
67end Physics
68end IndisputableMonolith