refined_shift_wallpaper_multiplier_forced_from_cubic_scale
plain-language theorem explainer
Fixing the cubic coefficient c to 12 in the refined shift affine expression forces the wallpaper multiplier u to equal 2. Mass-layer perturbation researchers cite this to close the O4 coefficient forcing in the J-cost bridge. The proof substitutes the fixed c into the hypothesis, isolates the base shift component via the channel form lemma, and invokes the base multiplier forcing theorem.
Claim. Assume $c = 12$ and refined_shift $= u W + L + (α^2 + c α^3)$, where $W$ is the number of wallpaper groups and $L$ is the ledger fraction. Then the wallpaper multiplier $u = 2$.
background
The module supplies the mass-layer J-cost perturbation bridge and certifies the Jcost(1+α) perturbative channel form together with the explicit α² + 12α³ radiative decomposition inside refined_shift. Alpha is the fine-structure constant. W abbreviates the number of wallpaper groups. Ledger fraction is the topological count from mass topology. Refined shift channel form states that refined_shift equals base_shift plus (α² + 12 α³). Base shift wallpaper multiplier forced states that in the affine family uW + ledger_fraction, canonical base_shift matching forces u = 2.
proof idea
Substitute the hypothesis c = 12 to obtain the refined shift equation with the explicit 12 α³ term. Apply linarith together with refined_shift_channel_form to isolate the base_shift equation. Invoke base_shift_wallpaper_multiplier_forced on the isolated equation to conclude u = 2.
why it matters
This supplies the forcing direction used by the downstream theorem refined_shift_wallpaper_iff_cubic_from_base_role, which packages the equivalence u = 2 ↔ c = 12 under fixed base-shift role. It closes one packaged route in the O4 perturbative coefficient forcing inside the J-Cost Perturbation module and links to the alpha derivation and mass topology ledger counts. In the Recognition framework it fixes the cubic radiative correction that enters the mass formula on the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.