module module

`IndisputableMonolith.Constants.ExternalAnchors`

show as: view Lean formalization →

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

generate prose now

used by (4)

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

IndisputableMonolith.Physics.NeutrinoSector module_import
IndisputableMonolith.Thermodynamics.ChemicalPotential module_import
IndisputableMonolith.Thermodynamics.HeatCapacity module_import
IndisputableMonolith.Thermodynamics.PhaseTransitions module_import

declarations in this module (36)

abbrev ExternalAnchorMarker L53
def c_SI L67
def hbar_SI L72
def h_SI L77
def e_SI L82
def kB_SI L87
def NA_SI L92
def G_SI L98
def G_SI_uncertainty L102
def alpha_CODATA L118
def alpha_CODATA_uncertainty L122
def alpha_inv_CODATA L126
def alpha_inv_CODATA_uncertainty L130
structure AlphaInvBounds L133
def alpha_inv_bounds L139
def electron_mass_kg L155
def electron_mass_MeV L159
def muon_mass_MeV L164
def proton_mass_MeV L169
def electron_muon_ratio_CODATA L174
def electron_muon_ratio_uncertainty L178
def proton_electron_ratio_CODATA L182
def proton_electron_ratio_uncertainty L186
structure MassRatioBounds L189
def mass_ratio_bounds L197
structure EmpiricalAnchors L210
def empiricalAnchors L224
def withinSigma L227
def within3Sigma L231
lemma c_SI_pos L236
lemma hbar_SI_pos L237
lemma G_SI_pos L238
lemma alpha_inv_CODATA_pos L239
lemma electron_mass_MeV_pos L240
lemma muon_mass_MeV_pos L241
lemma proton_mass_MeV_pos L242