electron_structural_mass — Recognition explainer

formal statement (Lean)

  47noncomputable def electron_structural_mass : ℝ :=

proof body

Definition body.

  48  lepton_yardstick * phi ^ (electron_rung - 8)
  49
  50/-- Dimensionless Structural Ratio to E_coh. -/

used by (40)

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

alphaG_pred_closed in IndisputableMonolith.Masses.AlphaGScoreCard decl_use
alphaG_pred_eq in IndisputableMonolith.Masses.AlphaGScoreCard decl_use
native_very_not_codata in IndisputableMonolith.Masses.AlphaGScoreCard decl_use
row_alphaG_pred in IndisputableMonolith.Masses.AlphaGScoreCard decl_use
row_alphaG_pred_eq in IndisputableMonolith.Masses.AlphaGScoreCard decl_use
electron_residue in IndisputableMonolith.Physics.ElectronMass.Defs decl_use
electron_structural_mass in IndisputableMonolith.Physics.ElectronMass.Defs decl_use
electron_structural_mass_forced in IndisputableMonolith.Physics.ElectronMass.Defs decl_use
electron_structural_ratio in IndisputableMonolith.Physics.ElectronMass.Defs decl_use
predicted_electron_mass in IndisputableMonolith.Physics.ElectronMass.Defs decl_use
gap_1332_bounds in IndisputableMonolith.Physics.ElectronMass.Necessity decl_use
structural_mass_bounds in IndisputableMonolith.Physics.ElectronMass.Necessity decl_use
predicted_mass_mu in IndisputableMonolith.Physics.LeptonGenerations.Defs decl_use
predicted_mass_tau in IndisputableMonolith.Physics.LeptonGenerations.Defs decl_use
predicted_mass_mu_lower in IndisputableMonolith.Physics.LeptonGenerations.Necessity decl_use
predicted_mass_mu_lower_tight in IndisputableMonolith.Physics.LeptonGenerations.Necessity decl_use
predicted_mass_mu_lower_v2 in IndisputableMonolith.Physics.LeptonGenerations.Necessity decl_use
predicted_mass_mu_upper in IndisputableMonolith.Physics.LeptonGenerations.Necessity decl_use
predicted_mass_mu_upper_tight in IndisputableMonolith.Physics.LeptonGenerations.Necessity decl_use
predicted_mass_mu_upper_v2 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
dm2_31_frac_pred_with_legacy_in_nufit_2sigma in IndisputableMonolith.Physics.NeutrinoSector decl_use
MassDisplayCalibration in IndisputableMonolith.Physics.NeutrinoSector decl_use
nu1_frac_pred_bounds in IndisputableMonolith.Physics.NeutrinoSector decl_use
nu2_frac_pred_bounds in IndisputableMonolith.Physics.NeutrinoSector decl_use

… and 10 more

depends on (5)

Lean names referenced from this declaration's body.

electron_rung in IndisputableMonolith.Physics.ElectronMass.Defs decl_use
electron_structural_mass in IndisputableMonolith.Physics.ElectronMass.Defs decl_use
lepton_yardstick in IndisputableMonolith.Physics.ElectronMass.Defs decl_use
electron_rung in IndisputableMonolith.RRF.Physics.ElectronMass.Defs decl_use
lepton_yardstick in IndisputableMonolith.RRF.Physics.ElectronMass.Defs decl_use