IndisputableMonolith.Verification.PDGComparison

declarations in this module (29)

• def alphaInv_CODATA_2022 L44
• def alphaInv_CODATA_2022_sigma L47
• def alphaInv_CODATA_2022_lo L50
• def alphaInv_CODATA_2022_hi L53
• def mass_electron_PDG L58
• def mass_electron_PDG_sigma L59
• def mass_muon_PDG L62
• def mass_muon_PDG_sigma L63
• def mass_tau_PDG L66
• def mass_tau_PDG_sigma L67
• def alphaInv_RS_lo L72
• def alphaInv_RS_hi L73
• theorem alphaInv_RS_lower_verified L80
• theorem alphaInv_RS_upper_verified L83
• theorem alphaInv_RS_contains_CODATA L92
• def alphaInv_RS_interval_width L103
• theorem alphaInv_RS_interval_width_eq L106
• def alphaInv_RS_relative_precision L111
• theorem alphaInv_RS_precision_sub_100ppm L115
• structure ComparisonResult L126
• def contains_exp L134
• def tension_sigma L138
• def alpha_result L143
• theorem alpha_result_contains_exp L151
• def alphaInv_RS_center L158
• theorem alphaInv_RS_center_eq L161
• def alphaInv_deviation L166
• theorem alphaInv_deviation_approx L169
• def alpha_summary L179