r0_sum
plain-language theorem explainer
The four sector base offsets r₀ (lepton, up quark, down quark, electroweak) sum exactly to 147. Anyone checking the O1 yardstick assignment principle or the structural identity Σ r₀ = V·W + E_passive cites this. The proof unfolds the four closed-form r₀ equalities and evaluates the resulting integer arithmetic.
Claim. The four sector yardstick offsets sum to $147$: $r_0(\mathrm{Lepton})+r_0(\mathrm{Up})+r_0(\mathrm{Down})+r_0(\mathrm{EW})=147$. With the closed forms $4W-6$, $2W+A$, $E-W$, and $3W+4$ (where $W=17$, $A=1$, $E=12$), the integer sum is $62+35+(-5)+55=147$.
background
Open Problem O1 asks why each particle sector receives a specific yardstick pair $(B_{\mathrm{pow}}, r_0)$ from the counting layer. The module's answer is that each sector couples to a distinct level of the 3-cube hierarchy: leptons to passive edges, up/EW to the active edge, down quarks to total edges.
The $r_0$ values are wallpaper-modulated integer offsets built from $W=17$ (wallpaper groups), the active-edge count $A=1$, and the total edge count $E=12$: $r_0(\mathrm{Lepton})=4W-6=62$, $r_0(\mathrm{Up})=2W+A=35$, $r_0(\mathrm{Down})=E-W=-5$, $r_0(\mathrm{EW})=3W+4=55$.
Passive edges are $E_{\mathrm{passive}}=E-A=11$. Cube vertex count is $V=8$. The $W$-multipliers ${4,2,-1,3}$ already sum to $V$, which is the combinatorial seed of the later identity $\sum r_0=V\cdot W+E_{\mathrm{passive}}$.
proof idea
Term-mode proof in two steps. First simp only rewrites each sector offset by its closed-form equality (r0_Lepton_eq, r0_UpQuark_eq, r0_DownQuark_eq, r0_Electroweak_eq), producing the concrete integer sum $62+35+(-5)+55$. Then norm_num discharges the arithmetic goal $147$. No induction or external lemmas beyond those four equalities.
why it matters
This is the numeric half of the O1 structural sum. Immediately downstream, r0_sum_eq_V_mul_W_add_Epassive rewrites $147$ as $V\cdot W+E_{\mathrm{passive}}=8\cdot 17+11$, the identity used by O1 filters. The choice-set theorem r0_sum_target_matches_principle then equates the abstract target constant to the live sector sum via this result.
In the Recognition framework the identity ties sector yardsticks to cube combinatorics ($V=8$ vertices of the 3-cube, eight-tick octave landmark T7) and to the wallpaper count $W=17$. It does not invent new physics constants; it certifies that the four assigned $r_0$ formulas are consistent with a single global budget $V W+E_{\mathrm{passive}}$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.