r0_sum_eq_V_mul_W_add_Epassive
plain-language theorem explainer
The four sector base offsets r₀ (lepton, up, down, electroweak) sum to V·W + E_passive. Anyone checking O1 yardstick filters or the sector↔cube coupling table cites this. Proof is a two-step calc: r0_sum gives 147, then native_decide matches the integer constants on the right-hand side.
Claim. The sum of the four sector base rung offsets equals the cube-vertex count times the wallpaper count plus the passive-edge count: $r_0(\mathrm{Lepton}) + r_0(\mathrm{Up}) + r_0(\mathrm{Down}) + r_0(\mathrm{EW}) = V \cdot W + E_{\mathrm{passive}}$, where $V = 2^D$ (with $D = 3$), $W$ is the wallpaper-group integer, and $E_{\mathrm{passive}}$ is the passive-edge integer of the recognition cube.
background
Open Problem O1 asks why each particle sector receives its particular $B_{\mathrm{pow}}$ and $r_0$ formula from the counting layer. The Yardstick Assignment Principle answers by coupling each sector to a distinct level of the 3-cube hierarchy (passive edges, active edge, total edges).
The $r_0$ layer consists of wallpaper-modulated integer offsets. With $W = 17$ (wallpaper groups) and cube edge data $E$, $A$, the formulas are $r_0(\mathrm{Lepton}) = 4W-6$, $r_0(\mathrm{Up}) = 2W+A$, $r_0(\mathrm{Down}) = E-W$, $r_0(\mathrm{EW}) = 3W+4$. The $W$-multipliers ${4,2,-1,3}$ sum to $8 = V = 2^D$, the vertex count of the $D$-cube forced by T8 ($D = 3$).
Upstream, cube_vertices is defined as $2^D$ and $D := 3$. The sibling lemma r0_sum already evaluates the left-hand side to the concrete integer 147. The identity $\sum r_0 = V\cdot W + E_{\mathrm{passive}}$ is the structural filter form used by O1 checks.
proof idea
Two-step calc. First rewrite the sector sum by the sibling r0_sum, which evaluates $r_0(\mathrm{Lepton})+r_0(\mathrm{Up})+r_0(\mathrm{Down})+r_0(\mathrm{EW})$ to $147$. Second, close equality of $147$ with $(V:(\mathbb{Z}))\cdot(W:(\mathbb{Z}))+(E_{\mathrm{passive}}:(\mathbb{Z}))$ by native_decide on the fully concrete integer constants ($V=8$, $W=17$, and the fixed passive-edge integer). No algebraic expansion of the individual $r_0$ formulas is needed here.
why it matters
This is the structural sum identity that O1 filters consume: $\sum r_0 = V\cdot W + E_{\mathrm{passive}}$. It certifies that the four wallpaper-modulated offsets are not independent numerology but close under the cube's vertex count $V=2^D=8$ (T8 forces $D=3$; the eight vertices are the eight-tick octave of T7).
Together with the companion $B_{\mathrm{pow}}$ partition identities in the same module, it supports the claim that sector yardsticks encode distinct couplings to the 3-cube edge network (leptons borrow $2E_p$ passive bits; quarks sit on active/total edges; EW sits on the active edge). The module frames this as the reason each sector gets its specific $B_{\mathrm{pow}}$ and $r_0$ formula.
No downstream consumers are wired yet in the graph (used_by is empty), so the lemma presently stands as a verified O1 checkpoint rather than an intermediate step inside a larger proved chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.