radiative_cubic_coeff_forced
plain-language theorem explainer
The declaration forces the cubic coefficient in the radiative correction expansion to equal 12 under canonical matching. Researchers deriving lepton masses or fine-structure perturbations in Recognition Science cite it to fix the O(alpha^3) term in J-cost channels. The short tactic proof invokes the canonical channel form, proves alpha positivity from bounds, equates the cubic terms by linear arithmetic, and cancels the nonzero alpha^3 factor.
Claim. If the radiative correction equals $alpha^2 + c alpha^3$, then the coefficient satisfies $c = 12$.
background
The module bridges mass-layer J-cost perturbations to canonical lepton-step definitions and certifies the Jcost(1 + alpha) perturbative channel form together with the explicit alpha^2 + 12 alpha^3 radiative decomposition. Alpha is the fine-structure constant, realized as the reciprocal of its inverse. Upstream structures include nuclear densities and photon fluxes occupying discrete phi-tiers, the canonical arithmetic object supplying realization-independent Peano invariants, and ledger factorization of the positive reals under multiplication with J-cost calibration.
proof idea
The proof obtains the canonical expression radiative_correction = alpha^2 + 12 * alpha^3 from the channel-form lemma. It extracts alpha positivity and nonzeroness from the supplied bounds via linarith. Linear arithmetic then equates the two cubic terms, after which right-multiplication cancellation on the nonzero alpha^3 factor yields c = 12.
why it matters
This result pins the cubic coefficient inside the radiative channel and directly supplies the parent theorem refined_shift_cubic_coeff_forced that extends the same forcing to base_shift plus the correction term. It completes the O4 perturbative closure for the mass layer, consistent with the phi-ladder, eight-tick octave, and alpha band (137.030, 137.039) landmarks of the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.