radiative_correction_bounds
plain-language theorem explainer
This lemma pins the total radiative correction between 0.0000578 and 0.0000580. Researchers deriving the refined electron mass shift in Recognition Science cite it to control the alpha-derived contributions. The proof unfolds the correction into its order-two and order-three pieces, invokes the separate alpha-squared and alpha-cubed bounds, and closes the target interval by linear arithmetic.
Claim. $0.0000578 < α² + 12 α³ < 0.0000580$
background
The module proves that the electron mass formula is forced from T8 ledger quantization and the geometric constants obtained earlier in the chain. The radiative correction is defined as the sum of the primary term α² and the secondary term E_total · α³, where E_total equals twelve from the three-dimensional hypercube edge count. Upstream lemmas supply the input intervals 0.0000532 < α² < 0.0000533 and 0.000000388 < α³ < 0.000000389.
proof idea
The term proof first simplifies the radiative correction expression using its definition together with the order-two, order-three, and E_total abbreviations. It then obtains the alpha-squared bounds and alpha-cubed bounds as hypotheses. The two-sided target inequality is closed by applying linear arithmetic to the resulting numerical comparisons.
why it matters
The lemma supplies the radiative correction interval required by the refined shift bounds lemma inside the same module. That result in turn supports the T9 necessity claim that the electron mass is forced from T8 and the geometric constants. The numerical bounds sit inside the Recognition Science alpha band and rely on D = 3 from the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.