mass_path_endogenous_replacement_complete
plain-language theorem explainer
Canonical mass-path formulas that carry the wallpaper count stay unchanged when the imported crystallographic constant is replaced by the endogenous cube-derived count. Auditors of the O6 sufficiency route in the mass framework cite this packaged invariance. The proof is a four-conjunct packaging of sibling rewrite lemmas already proved in the module.
Claim. The cube-derived wallpaper count equals the mass-topology count $W$, the ledger fraction equals $(W_{\mathrm{cube}}+E_{\mathrm{total}})/(4E_{\mathrm{passive}})$, the base shift equals $2W_{\mathrm{cube}}$ plus that ledger fraction, and the muon-tau step equals the number of $D$-cube faces minus $(2W_{\mathrm{cube}}+D)/2$ times the fine-structure constant $\alpha$.
background
The module formalizes the sufficiency route for obligation O6 in the mass framework: canonical mass-path formulas must be unchanged when the imported crystallographic wallpaper count is replaced by an endogenous cube quantity $W_{\mathrm{cube}}=E_{\mathrm{passive}}+F$ at spatial dimension $D=3$.
Here $D$ is the forced spatial dimension (value 3), cube faces equal $2D$, and $\alpha$ is the electromagnetic fine-structure constant. The mass path uses four $W$-bearing identities: equality of the two wallpaper counts, a ledger-fraction rewrite, a base-shift rewrite, and a muon-tau step rewrite that mixes cube faces, $W$, $D$, and $\alpha$.
Upstream constants supply $\alpha:=1/\alpha^{-1}$ and $\mathrm{cube_faces}(d)=2d$, so at $D=3$ one has six faces. The present theorem only packages the four endogenous rewrites; it does not re-derive those constants.
proof idea
Term-mode packaging via a single refine of a 4-tuple. The four conjuncts are discharged by the sibling lemmas already in the module: endogenous $W$ equals the mass-topology $W$; ledger fraction rewrites under endogenous $W$; base shift rewrites under endogenous $W$; and the muon-tau step rewrites under endogenous $W$. No fresh algebra occurs at this site; the conjunction is the closure certificate.
why it matters
This is the packaged closure of the wallpaper-sufficiency route for O6: every canonical $W$-bearing mass-path formula is invariant under $W\mapsto W_{\mathrm{cube}}$. Downstream mass-path consumers can therefore treat the cube-derived count as interchangeable with the crystallographic import. The certificate sits on $D=3$ from the forcing chain and on the cube-face count $2D$, and it retains $\alpha$ in the muon-tau step exactly as written. In the present dependency graph it is a terminal verification node (no recorded parents yet), so its role is to seal the sufficiency claim rather than to feed a further theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.