radiative_correction_channel_form
plain-language theorem explainer
The theorem states that the total radiative correction equals the square of the fine-structure constant plus twelve times its cube. Researchers deriving perturbative mass corrections in the Recognition Science framework cite this for the explicit cubic-channel form in the mass topology path. The proof is a one-line wrapper that invokes the channel decomposition lemma.
Claim. The total radiative correction equals the square of the fine-structure constant plus twelve times its cube: $radiative_correction = alpha^2 + 12 alpha^3$.
background
This declaration belongs to the Mass-Layer J-Cost Perturbation Bridge module, which upstreams the O4 perturbative closure into the Masses namespace and certifies the J-cost(1+α) channel form together with the explicit radiative decomposition. The fine-structure constant α is defined as the reciprocal of alphaInv. The total radiative correction is defined as the sum of the second-order and third-order correction terms.
proof idea
The proof is a one-line wrapper that applies the radiative_correction_channel_decomposition lemma from the upstream mass topology definitions.
why it matters
This supplies the explicit α² + 12α³ decomposition that feeds the refined_shift_channel_form theorem and the radiative_cubic_coeff_forced theorem, which forces the cubic coefficient to 12. It closes the O4 perturbative path in the mass topology and aligns with the alpha derivation in the Recognition Science constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.