radiative_correction
plain-language theorem explainer
The radiative_correction definition sums the second-order self-energy term alpha squared with the third-order edge-coupling term E_total times alpha cubed. Physicists deriving the electron mass shift via the refined ledger fraction would cite this when isolating perturbative contributions from the geometric base. It is assembled as a direct sum of the two order-specific correction definitions.
Claim. The total radiative correction is defined as $alpha^2 + E_{total} alpha^3$, where $E_{total}$ is the number of edges in the cubic ledger $Q_3$.
background
In the MassTopology module the refined ledger fraction for the electron mass shift is built from base geometric terms (involving W, E_total, E_passive) plus explicit radiative corrections. The upstream definition correction_order_2 supplies the primary term alpha squared as the second-order self-energy contribution. The upstream definition correction_order_3 supplies the secondary term E_total times alpha cubed, capturing coupling across the twelve edges of the cubic structure.
proof idea
This is a one-line definition that adds the second-order correction to the third-order correction.
why it matters
This definition supplies the radiative component decomposed in downstream theorems such as radiative_correction_channel_form (which proves equality to alpha squared plus twelve alpha cubed) and radiative_cubic_coeff_forced (which forces the cubic coefficient to twelve). It is added to base_shift to produce refined_shift and is bounded in the ElectronMass.Necessity lemma. Within the Recognition framework it completes the T9 topology step by furnishing the explicit alpha squared plus E_total alpha cubed channel that matches the empirical shift to within two times ten to the minus seven.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.