r0_sum_decomposition
plain-language theorem explainer
Integer identity 147 = 8·17 + 11, the arithmetic skeleton of the four-sector r₀ sum as V·W + E_passive. Anyone auditing Yardstick Assignment (O1) bookkeeping cites it when checking that the wallpaper-modulated offsets close. Proof is a one-line norm_num evaluation.
Claim. The equality $147 = 8 \cdot 17 + 11$ holds in $\mathbb{Z}$.
background
Module O1 (Yardstick Assignment Principle) asks why each particle sector inherits a specific B_pow and r₀ formula from the 3-cube counting layer. The four r₀ offsets are wallpaper-modulated:
- lepton: $4W-6=62$
- up: $2W+A=35$
- down: $E-W=-5$
- electroweak: $3W+4=55$
with $W=17$ (wallpaper groups), $E=12$ (cube edges), $A=1$ (active edge). Their sum is $62+35+(-5)+55=147$. Writing each offset as $r_0=mW+c$ with multipliers ${4,2,-1,3}$ (summing to $V=8$, the cube vertex count) and constants ${-6,1,12,4}$ (summing to $11=E_{\mathrm{passive}}$) yields the closed form $V\cdot W+E_{\mathrm{passive}}=8\cdot17+11$.
This declaration isolates that pure integer identity. Sibling lemmas package the sector-wise formulas and the equality of the r₀ sum to $V\cdot W+E_{\mathrm{passive}}$.
proof idea
One-line tactic proof: norm_num reduces both sides in $\mathbb{Z}$ and closes by reflexivity. No lemmas are invoked; the statement is bare arithmetic.
why it matters
Closes the arithmetic side of the r₀ bookkeeping inside Open Problem O1. The module's structural claim is that the W-multipliers ${4,2,-1,3}$ sum to the cube vertex count $V=8$ (eight-tick / $2^3$ landmark) and the constant terms sum to the passive-edge count $11$, so the four sector offsets total $V\cdot W+E_{\mathrm{passive}}$. This theorem is the numerical witness for that decomposition.
No downstream consumers are wired yet (used_by empty); siblings r0_sum and r0_sum_eq_V_mul_W_add_Epassive are the natural parents once the sector formulas are assembled. It does not touch mass-ladder physics beyond the counting layer, nor the B_pow partition identities treated separately in the same module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.