correction_order_3
plain-language theorem explainer
The declaration defines the third-order radiative correction term as the product of the total number of edges in the cubic ledger and the cube of the fine-structure constant. Researchers assembling the refined ledger fraction for the electron mass in the Recognition Science T9 topology would cite this term when summing the full radiative shift. The definition is a direct one-line algebraic expression that multiplies the imported E_total by alpha cubed.
Claim. The third-order correction is $E_{total} alpha^3$, where $E_{total}=12$ counts the edges of the cubic ledger $Q_3$ and $alpha$ is the fine-structure constant.
background
The MassTopology module derives the topological shift delta for the electron mass from the geometry of the cubic ledger Q3. E_total is defined locally as cube_edges 3, giving the integer 12 that counts all edges; the same symbol is also imported from Masses.Anchor as cube_edges D with D=3. Alpha is imported from Constants.Alpha as the reciprocal of the derived alphaInv.
proof idea
This is a one-line definition that directly multiplies the imported E_total by the imported alpha raised to the third power. It applies no lemmas beyond the definitions of E_total and alpha; the expression is written verbatim in the body.
why it matters
The term supplies the alpha^3 contribution inside the total radiative_correction definition, which is then invoked by radiative_correction_bounds to establish the numerical interval (0.0000578, 0.0000580) for the electron-mass shift. It completes the third-order edge-coupling piece of the T9 formula delta = 2W + (W + E_total)/(4 E_passive) + alpha^2 + E_total alpha^3, achieving the reported 2 times 10^{-7} match to empirical data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.