IndisputableMonolith.Physics.ElectronGMinus2ScoreCard
The module assembles the P1-C05 leading electron anomaly prediction in Recognition Science. It builds a scorecard from imported alpha inverse bounds to certify the leading Schwinger contribution to the electron g-2. The structure consists of row definitions for the leading term, codata, positivity checks, and a final certificate theorem.
claimThe leading electron anomaly $a_e$ is certified when the inverse fine-structure constant lies in the interval supplied by the AlphaBounds module, yielding the scorecard certificate for the prediction.
background
Recognition Science derives the fine-structure constant from the J-uniqueness condition and the phi self-similar fixed point in the T0-T8 forcing chain. The imported Alpha module supplies the RS-native definition of alpha with the given constants, while AlphaBounds provides rigorous interval arithmetic bounds on alpha inverse. The module operates in the physics domain to apply these constants to the electron anomalous magnetic moment.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The module implements the P1-C05 leading electron anomaly prediction. It feeds the certified scorecard into the Recognition Science derivation of particle properties from the functional equation and RCL, using the alpha band (137.030, 137.039).
scope and limits
- Does not compute higher-order QED corrections to the anomaly.
- Does not compare the prediction against experimental values.
- Does not derive the alpha bounds, only imports them.
- Does not address anomalies for 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