abbrev definition def or abbrev

`Mass`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  58abbrev Mass := ℝ

used by (40)

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

information_balance_gives_phi in IndisputableMonolith.Astrophysics.ObservabilityLimits decl_use
ml_geometric_bounds in IndisputableMonolith.Astrophysics.ObservabilityLimits decl_use
PhysicalCertificate in IndisputableMonolith.Certificates.Standard decl_use
Dimension in IndisputableMonolith.Constants.Dimensions decl_use
dim_T in IndisputableMonolith.Constants.Dimensions decl_use
proton_electron_ratio_uncertainty in IndisputableMonolith.Constants.ExternalAnchors decl_use
hbarQuantum_eq_Ecoh in IndisputableMonolith.Constants.RSNativeUnits decl_use
mass_raw in IndisputableMonolith.Constants.RSNativeUnits decl_use
momentumQuantum_eq_cohQuantum in IndisputableMonolith.Constants.RSNativeUnits decl_use
planckMass_rs in IndisputableMonolith.Constants.RSNativeUnits decl_use
to_kg in IndisputableMonolith.Constants.RSNativeUnits decl_use
Axion in IndisputableMonolith.Cosmology.DarkMatter decl_use
dmIsNot in IndisputableMonolith.Cosmology.DarkMatter decl_use
WIMP in IndisputableMonolith.Cosmology.DarkMatter decl_use
w_mass_atlas_measurement in IndisputableMonolith.Cosmology.WMassAnomalyStructure decl_use
w_mass_implies_ew_scale in IndisputableMonolith.Cosmology.WMassAnomalyStructure decl_use
w_z_mass_ratio in IndisputableMonolith.Cosmology.WMassAnomalyStructure decl_use
cycleLength in IndisputableMonolith.Derivations.MassToLight decl_use
mass_geometric in IndisputableMonolith.Foundation.CKMHierarchyFromPhiLadder decl_use
quark_rungs_strict_ordering in IndisputableMonolith.Foundation.CKMHierarchyFromPhiLadder decl_use
top_rung in IndisputableMonolith.Foundation.CKMHierarchyFromPhiLadder decl_use
dirac_mass_pos in IndisputableMonolith.Foundation.DiracEquationFromJCost decl_use
jcost_cosh_is_gamma_minus_one in IndisputableMonolith.Foundation.SpecialRelativityDeep decl_use
D3_unique_viable in IndisputableMonolith.Foundation.SpectralEmergence decl_use
mass_rung_step in IndisputableMonolith.Foundation.SpectralEmergence decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
quark_lepton_ratio in IndisputableMonolith.Foundation.SpectralEmergence decl_use
SpectralEmergenceCert in IndisputableMonolith.Foundation.SpectralEmergence decl_use
alpha_gravity_pos in IndisputableMonolith.Gravity.GravityParameters decl_use
small_strain_hamiltonian_valid in IndisputableMonolith.Gravity.UltramassiveBH decl_use

… and 10 more