refined_shift_channel_form
plain-language theorem explainer
The theorem equates the refined shift in mass topology to the base geometric shift plus the explicit radiative correction α² + 12α³. Mass-layer calculations in the Recognition framework cite it when decomposing perturbative corrections for lepton hierarchies. The proof is a one-line term wrapper that applies congruence to the upstream radiative correction decomposition.
Claim. refined_shift = base_shift + (α² + 12 α³)
background
In the JCostPerturbation module the refined shift decomposes total mass corrections into a geometric base term plus radiative channels tied to the fine-structure constant. The module certifies the Jcost(1+α) perturbative form and the explicit α² + 12α³ decomposition used in mass topology paths. Upstream, alpha is the fine-structure constant 1/alphaInv, while radiative_correction_channel_form establishes the radiative part as α² + 12α³.
proof idea
The term proof invokes simpa with the definition of refined_shift on a congruence argument that substitutes the radiative correction decomposition directly into the base shift expression.
why it matters
This supplies the explicit channel form required by the O4 channel closure certificate, which combines refined_shift with ledger fractions for electron-muon-tau refinements. It also feeds the wallpaper multiplier forcing theorem that derives the coefficient u=2 once the cubic scale is fixed at 12. The result closes the perturbative path from J-uniqueness through the phi-ladder to mass formulas in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.