electron_structural_mass — Recognition explainer

formal statement (Lean)

 161noncomputable def electron_structural_mass : ℝ :=

proof body

Definition body.

 162  lepton_yardstick * phi ^ (electron_rung - (octave_period : ℤ))
 163
 164/-- 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_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
nu2_pred_bounds in IndisputableMonolith.Physics.NeutrinoSector decl_use

… and 10 more

depends on (6)

Lean names referenced from this declaration's body.

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