IndisputableMonolith.Physics.ElectronGMinus2ScoreCard
The ElectronGMinus2ScoreCard module assembles the leading electron anomaly prediction labeled P1-C05 in Recognition Science. It imports interval bounds on alpha inverse to build scorecard rows and a holding certificate for the anomalous magnetic moment. Physicists working on low-order QED tests would cite these interval results. The module organizes definitions and certificates from the alpha bounds without containing proofs itself.
claimThe leading electron anomaly prediction $a_e$ is certified to lie in an interval derived from the fine-structure constant bounds $137.030 < α^{-1} < 137.039$, with the scorecard certificate holding for the leading Schwinger term and codata contributions.
background
This module sits in the Physics domain and imports the definition of the fine-structure constant together with rigorous interval bounds on its inverse. The upstream AlphaBounds module supplies symbolic interval arithmetic ensuring $α^{-1}$ lies inside (137.030, 137.039). These bounds feed directly into positivity statements and bracketed intervals for the anomaly rows.
proof idea
This is a definition module, no proofs. The structure consists of importing the alpha and alpha-bounds modules, then declaring sibling rows for the leading term, codata, positivity lemmas, and the top-level scorecard certificate.
why it matters in Recognition Science
The module fills proposition P1-C05 by supplying the leading electron anomaly prediction. It supplies the ElectronGMinus2ScoreCardCert whose holding statement closes the scorecard. The construction ties the alpha interval directly to the Recognition Science constants and the eight-tick octave structure.
scope and limits
- Does not compute higher-loop QED corrections beyond the listed rows.
- Does not compare the prediction against experimental a_e data.
- Does not derive the alpha interval from the forcing chain.
- Does not address the muon anomaly or other leptons.
depends on (2)
declarations in this module (12)
-
def
row_electron_ae_leading -
def
row_electron_ae_codata -
theorem
alphaInv_pos -
theorem
row_electron_ae_leading_eq -
theorem
ae_den_pos -
theorem
row_electron_ae_leading_lower -
theorem
row_electron_ae_leading_upper -
theorem
row_electron_ae_leading_bracket -
theorem
row_electron_ae_codata_pos -
theorem
row_electron_ae_schwinger_relative_residual -
structure
ElectronGMinus2ScoreCardCert -
theorem
electronGMinus2ScoreCardCert_holds