IndisputableMonolith.Physics.ElectronGMinus2ScoreCard

declarations in this module (12)

• def row_electron_ae_leading L45
• def row_electron_ae_codata L49
• theorem alphaInv_pos L51
• theorem row_electron_ae_leading_eq L54
• theorem ae_den_pos L59
• theorem row_electron_ae_leading_lower L62
• theorem row_electron_ae_leading_upper L84
• theorem row_electron_ae_leading_bracket L107
• theorem row_electron_ae_codata_pos L112
• theorem row_electron_ae_schwinger_relative_residual L117
• structure ElectronGMinus2ScoreCardCert L125
• theorem electronGMinus2ScoreCardCert_holds L133