r0_values
plain-language theorem explainer
The four sector φ-exponent offsets evaluate to the fixed integers 62 (lepton), 35 (up quark), −5 (down quark), and 55 (electroweak). Anyone auditing the yardstick mass ladder or the O1 sector-assignment table cites this bundle. The proof is a pure term-mode conjunction of the four sector-wise evaluation lemmas.
Claim. The derived $\varphi$-exponent offsets satisfy $r_0(\mathrm{Lepton})=62$, $r_0(\mathrm{Up\ quark})=35$, $r_0(\mathrm{Down\ quark})=-5$, and $r_0(\mathrm{Electroweak})=55$.
background
In the Anchor layer, each particle sector carries a derived integer offset $r_0$ that enters the sector yardstick $A_s=2^{B_{\mathrm{pow}}}E_{\mathrm{coh}}\varphi^{r_0}$. These offsets are not free parameters: they are built from the wallpaper count $W=17$ and the 3-cube edge data ($E_{\mathrm{total}}=12$, active edges $A=1$).
Explicitly, $r_0(\mathrm{Lepton})=4W-6$, $r_0(\mathrm{Up})=2W+A$, $r_0(\mathrm{Down})=E-W$, and $r_0(\mathrm{EW})=3W+4$. The module frames Open Problem O1: why each sector couples to its particular cube-hierarchy level, producing exactly these wallpaper-modulated formulas.
Upstream, four separate evaluation lemmas already reduce each formula under the concrete constants $W$, $E$, $A$ and obtain the integers 62, 35, −5, 55.
proof idea
Term-mode packaging only. The proof is the 4-tuple constructor applied to the four upstream equalities r0_Lepton_eq, r0_UpQuark_eq, r0_DownQuark_eq, and r0_Electroweak_eq. Each of those lemmas is itself a one-line simp of the defining formula followed by norm_num on the wallpaper and cube constants; no new arithmetic is performed here.
why it matters
This declaration freezes the numerical $r_0$ column of the O1 yardstick-assignment table. Together with the companion $B_{\mathrm{pow}}$ values it supplies the full sector yardstick that feeds the RS mass formula (yardstick times $\varphi$ raised to rung offset). The module notes that the $W$-multipliers ${4,2,-1,3}$ sum to $V=8$, tying the offsets back to the cube vertex count and the eight-tick octave (T7). No downstream consumers are wired yet; the lemma is the verified lookup table for any later mass or coupling identity that needs the four concrete integers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.