refined_shift_wallpaper_iff_cubic_from_base_role
plain-language theorem explainer
Under the fixed base-shift role, matching the affine form of refined_shift to base_shift plus the quadratic-cubic perturbation forces an equivalence: the wallpaper multiplier u equals 2 precisely when the cubic coefficient c equals 12. Mass-layer modelers in Recognition Science would cite this to close the O4 perturbative coefficients for lepton steps. The proof is a term-mode construction that invokes the joint affine forcing lemma to obtain the pair (u=2, c=12) and then splits the biconditional via constructor and exact.
Claim. Assume base_shift = u W + ledger_fraction and refined_shift = u W + ledger_fraction + (α² + c α³). Then u = 2 if and only if c = 12.
background
The module supplies the O4 perturbative closure for J-cost perturbations in the Masses namespace, tying the canonical lepton-step definitions to the explicit radiative decomposition α² + 12 α³ inside refined_shift. W denotes the wallpaper-group count (17) that appears as the geometric multiplier in the affine base-shift role; ledger_fraction is the fixed fractional offset extracted from mass-topology ledger counts. The upstream joint-forcing theorem refined_shift_full_affine_forced_from_base_role states that once base_shift is fixed in the form u W + ledger_fraction, any matching refined_shift of the stated affine-plus-perturbation form forces both u = 2 and c = 12 simultaneously.
proof idea
The term proof first applies refined_shift_full_affine_forced_from_base_role to the two hypotheses, obtaining the pair u = 2 ∧ c = 12. It then uses constructor to build the biconditional; the forward direction extracts the second component of the pair, while the reverse direction invokes refined_shift_wallpaper_multiplier_forced_from_cubic_scale under the assumption c = 12.
why it matters
The declaration completes the coefficient-forcing package for the mass-layer J-cost bridge, fixing the wallpaper multiplier and cubic channel that enter the refined-shift expression used in lepton-generation derivations. It directly supports the mass-topology ledger_fraction and base_shift definitions that feed the phi-ladder mass formula. No open scaffolding remains inside the module; the result is a proved leaf in the O4 closure chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.