r0_sum_from_cube
plain-language theorem explainer
The four sector r₀ offsets, expanded via their wallpaper formulas in W=17, sum to 147. Anyone auditing the Yardstick Assignment Principle (O1) cites this as the closed arithmetic check Σ r₀ = V·W + E_passive. Proof is a one-line norm_num evaluation of the integer identity.
Claim. The integer identity $4\cdot 17+(-6)+(2\cdot 17+1)+(12-17)+(3\cdot 17+4)=147$ holds. Equivalently, writing each sector offset in wallpaper form, $\sum r_0=V\cdot W+E_{\mathrm{passive}}=8\cdot 17+11=147$.
background
Open Problem O1 asks why each particle sector receives a specific yardstick power $B_{\mathrm{pow}}$ and offset $r_0$ from the counting layer. The module's answer is the Assignment Principle: each sector couples to a distinct level of the 3-cube hierarchy (passive edges, active edge, total edges), and the formulas encode that coupling.
The $r_0$ values are wallpaper-modulated offsets built from $W=17$ (wallpaper groups), with cube counts $V=8$ vertices, $E=12$ total edges, active edge $A=1$, and passive edges $E_{\mathrm{passive}}=11$:
- lepton: $4W-6=62$
- up: $2W+A=35$
- down: $E-W=-5$
- electroweak: $3W+4=55$
The $W$-multipliers ${4,2,-1,3}$ sum to $V=8$, so the structural identity is $\sum r_0=V\cdot W+E_{\mathrm{passive}}$. Upstream, $B_{\mathrm{pow}}$ is defined sectorwise from the same cube edge counts (lepton $-2E_p$, up $-A$, down $2E-1$, EW $+A$).
proof idea
Pure closed arithmetic. The tactic norm_num evaluates the fully expanded integer expression on $\mathbb{Z}$ and discharges equality to 147. No lemmas are invoked; the identity is the concrete expansion of the four sector formulas already recorded in the module table.
why it matters
This is the arithmetic spine of the Yardstick Assignment Principle (O1): once the four $r_0$ formulas are written in $W$ and cube counts, their sum must close to $V\cdot W+E_{\mathrm{passive}}=147$. The sibling identity $\sum r_0=V\cdot W+E_{\mathrm{passive}}$ packages the same fact structurally; the present theorem is the fully expanded numerical witness.
In the broader RS mass ladder, $r_0$ enters the rung offset of the yardstick formula (mass $\propto\varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$). Closing $\sum r_0$ confirms that the sector offsets are not free parameters but a partition of a single cube-plus-wallpaper total. No downstream theorem currently depends on this declaration; it stands as a verification checkpoint inside the O1 module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.