base_shift_wallpaper_multiplier_forced
plain-language theorem explainer
The theorem forces the wallpaper multiplier coefficient u to equal 2 in any affine expression of base_shift as uW plus the ledger fraction. Mass-layer perturbation calculations cite it to fix the leading term before adding alpha corrections in the J-cost expansion. The short tactic proof recovers the canonical base_shift form by simplification, equates the two representations via linear arithmetic, and cancels the nonzero W factor.
Claim. If the base shift admits the affine representation $base_shift = u W + ell$, where $W$ is the wallpaper number and $ell$ the ledger fraction, then $u = 2$.
background
The module supplies the Lean closure package for O4 coefficient forcing in the mass-layer J-cost perturbation bridge and ties it to canonical lepton-step definitions. Base_shift is the leading term in the mass-topology J-cost expansion; it is canonically fixed as 2W plus the ledger fraction, with W the wallpaper number. Upstream results include the canonical arithmetic object (realization-independent Peano surface) and the spectral edge count E = D * 2^(D-1) that constrain the geometric constants on the mass ladder.
proof idea
The tactic proof first simplifies to obtain the canonical expression base_shift = 2W + ledger_fraction. Linear arithmetic equates the hypothesis to this form, isolating uW = 2W. Non-vanishing of W is decided natively, after which right-multiplication cancellation yields u = 2.
why it matters
This supplies the base multiplier forcing invoked by refined_shift_full_affine_forced_from_base_role (which jointly forces u = 2 and c = 12) and by refined_shift_wallpaper_multiplier_forced_from_cubic_scale (which recovers u = 2 once c = 12 is known). It anchors the leading term of the refined shift to the wallpaper multiplier, closing the O4 perturbative channel in the Recognition Science mass formula on the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.