correction_order_2
plain-language theorem explainer
correction_order_2 supplies the quadratic radiative term α² inside the refined ledger fraction δ for the electron mass shift. Lepton mass modelers cite it when assembling the T9 topological formula that matches empirical ratios to 2×10^{-7}. The declaration is a direct one-line abbreviation of the imported alpha constant.
Claim. The second-order radiative correction is defined by $correction = α^2$.
background
Module MassTopology derives the refined ledger fraction δ for the electron mass under T9 topology. The formula is δ = 2W + (W + E_total)/(4 E_passive) + α² + E_total α³, where W = 17 (wallpaper groups), E_total = 12 (cube edges), and E_passive = 11 (passive edges). Alpha is the fine-structure constant imported from Constants.Alpha as 1/alphaInv. The upstream E definition from SpectralEmergence gives the D-cube edge count D × 2^{D-1}.
proof idea
One-line definition that directly sets the symbol to alpha squared using the imported alpha constant.
why it matters
The definition supplies the α² term required by the T9 refined shift formula. It is invoked in downstream results such as step_e_mu_channel_split and o4_channel_closure_certificate to enforce the canonical e→μ geometric match. The term closes the one-loop self-energy contribution in the Recognition Science mass ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.