base_shift_rewrite_endogenous
plain-language theorem explainer
The mass-path base shift equals twice the endogenous cube wallpaper count plus the cube-rewritten ledger fraction, so it is unchanged when the imported crystallographic constant is swapped for W_from_cube. Citation target for anyone auditing O6 sufficiency of the lepton/mass ladder. Proof is a two-step calc: unfold the base-shift definition, then substitute the endogenous W equality and the ledger-fraction rewrite.
Claim. The base shift equals $2 W_{\mathrm{cube}} + \dfrac{W_{\mathrm{cube}} + E_{\mathrm{total}}}{4 E_{\mathrm{passive}}}$, where $W_{\mathrm{cube}}$ is the endogenous cube-derived wallpaper count at $D=3$ (replacing the imported crystallographic constant).
background
This module formalizes the sufficiency route for O6 in the mass framework: canonical mass-path formulas must stay the same when the imported crystallographic constant (wallpaper group count) is replaced by the endogenous cube quantity $W_{\mathrm{cube}} = E_{\mathrm{passive}} + F$ at spatial dimension $D=3$.
The base shift is the real combination $2W + \mathrm{ledger_fraction}$ used downstream in the mass ladder. Here $W$ is the wallpaper count appearing in mass topology, and the ledger fraction is the rational $(W + E_{\mathrm{total}})/(4 E_{\mathrm{passive}})$. Sibling results already give $W = W_{\mathrm{cube}}$ and the corresponding ledger-fraction rewrite under that replacement.
The local goal is invariance bookkeeping only: show each $W$-bearing formula is literally equal after the endogenous swap, not re-derive masses or coupling constants.
proof idea
Obtain the cast equality $(W:\mathbb{R})=(W_{\mathrm{cube}}:\mathbb{R})$ from the sibling endogenous identification of $W$ with $W_{\mathrm{cube}}$ (symmetry of that equality, then exact_mod_cast).
Then run a two-line calc: first unfold the definition of the base shift to $2W + \mathrm{ledger_fraction}$; second rewrite with the cast equality and the sibling ledger-fraction rewrite, which replaces the ledger term by $(W_{\mathrm{cube}}+E_{\mathrm{total}})/(4 E_{\mathrm{passive}})$. Both steps are simp with those two facts.
why it matters
This is one of the four conjuncts packaged by mass_path_endogenous_replacement_complete, the module's closure theorem: all canonical $W$-bearing mass-path formulas are invariant under replacing imported wallpaper groups by endogenous $W_{\mathrm{cube}}$. Downstream that package is the verification witness that the mass path does not secretly depend on an external crystallographic import.
In the broader Recognition Science stack this supports the mass-ladder side of the forcing chain at $D=3$ (T8) and the eight-tick / cube geometry that produces $W_{\mathrm{cube}}$. It does not itself compute particle masses; it certifies that the base-shift input to those formulas is endogenous.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.