refined_shift_cubic_coeff_forced
plain-language theorem explainer
The theorem shows that matching the refined shift to the base shift plus alpha squared plus c times alpha cubed forces the cubic coefficient c to equal 12. Researchers deriving lepton mass spectra from J-cost perturbations would cite it to fix the O4 radiative term. The tactic proof reduces the hypothesis to the canonical radiative correction via simplification and linear arithmetic, then invokes the prior cubic coefficient result.
Claim. If the refined shift equals the base shift plus the sum of the square of the fine-structure constant and $c$ times its cube, then $c=12$.
background
This declaration belongs to the Mass-Layer J-Cost Perturbation Bridge module, which supplies the O4 perturbative closure for the J-cost(1+α) channel and certifies the explicit α² + 12α³ radiative decomposition inside refined_shift. The module ties these expansions to canonical lepton-step definitions and geometric evaluations of zeroth-order constants. It imports the fine-structure constant α from Constants.Alpha (defined as 1/αInv) together with forcing structures from MagnitudeOfMismatch and UniversalForcingSelfReference.
proof idea
The proof first uses simp on the refined_shift definition to obtain refined_shift = base_shift + radiative_correction. Linear arithmetic then equates radiative_correction to the given α² + cα³ expression. The prior theorem radiative_cubic_coeff_forced is applied directly to conclude c = 12.
why it matters
The result supplies the cubic coefficient for the refined_shift case and is invoked by the downstream joint affine-family theorem refined_shift_full_affine_forced_from_base_role, which additionally forces the base-shift multiplier u to 2. It completes the O4 coefficient forcing step inside the Masses namespace, linking to the Recognition Science alpha band and the phi-ladder mass formula. No open scaffolding remains.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.