refined_shift
plain-language theorem explainer
The refined shift assembles the base topological contribution from wallpaper groups and ledger fractions with second- and third-order radiative corrections to give the complete predicted adjustment for the electron mass. Researchers deriving masses via the phi-ladder and J-cost perturbations would reference this value when closing the O4 channel or forcing cubic coefficients. The definition is a direct sum of the base shift and the total radiative correction.
Claim. The refined shift is defined by the equation $δ = δ_{base} + δ_{rad}$, where $δ_{base} = 2W +$ ledger fraction encodes the geometric contribution from the cubic ledger and $δ_{rad} = α² + 12α³$ supplies the total radiative correction.
background
This module develops the topological shift required for the electron mass under the T9 topology construction. The base shift supplies the geometric part 2W plus the ledger fraction that encodes the coupling ratio from the cubic ledger Q3 geometry with W = 17 wallpaper groups, E_total = 12 edges, and E_passive = 11 passive edges. The radiative correction adds the second-order self-energy term α² together with the third-order edge-coupling term scaled by the number of edges.
proof idea
The definition is a direct one-line sum of the base shift and the radiative correction. It inherits the explicit forms from the upstream definitions without further reduction.
why it matters
This definition supplies the complete predicted shift that feeds into the O4 channel closure certificate and the forcing theorems for the cubic radiative coefficient. It realizes the T9 topology step by packaging the geometric base from wallpaper symmetries and passive edges with the α² + 12α³ radiative channels. Downstream results such as refined_shift_channel_form and refined_shift_cubic_coeff_forced use it to enforce the canonical value c = 12 and close the ledger fraction construction for the electron mass hypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.