base_shift_eq_34_plus_29_over_44
plain-language theorem explainer
base_shift equals 34 plus 29/44 as the zeroth-order geometric term in the J-cost perturbation for masses. Lepton mass modelers cite it to fix the affine W-multiplier base before radiative corrections. The proof is a short calc that substitutes W equals 17 from mass topology counts and the ledger fraction 29/44 into the definition base_shift equals 2W plus ledger fraction.
Claim. In the affine family with multiplier 2 and wallpaper count W, the base shift satisfies $base_shift = 34 + 29/44$.
background
The JCostPerturbation module supplies the O4 perturbative closure for masses, linking Jcost(1+α) channel forms to lepton-step definitions and the explicit zeroth-order constants used in refined_shift. W is the wallpaper group count fixed at 17; ledger_fraction is the electron-break component fixed at 29/44. These appear in the affine expression base_shift = 2W + ledger_fraction with u forced to 2.
proof idea
The tactic proof first obtains W = 17 by exact_mod_cast from mass_topology_counts. A calc block rewrites base_shift via simp on its definition as 2W plus ledger_fraction, substitutes the known values from ledger_fraction_eq_29_over_44, and finishes with ring.
why it matters
This supplies the explicit numeric zeroth-order geometric part of the refined shift, completing a required evaluation inside the O4 coefficient forcing package. It anchors the base for subsequent radiative terms in lepton generation masses. The result sits downstream of mass_topology_counts and ledger_fraction_eq_29_over_44 and supports the mass formula on the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.