r0_lepton_ew_depth_gap
plain-language theorem explainer
The lepton and electroweak r₀ offsets differ by exactly W−10 (wallpaper count minus ten), i.e. 62−55=7. Anyone auditing sector yardsticks or the O1 assignment table cites this identity. The proof is a short numerical reduction from the closed forms r₀(Lepton)=62 and r₀(EW)=55.
Claim. The $\varphi$-exponent offset of the lepton sector minus that of the electroweak sector equals the wallpaper-group count minus ten: $r_0(\mathrm{Lepton})-r_0(\mathrm{Electroweak})=W-10$, where $W=17$ is the number of 2D wallpaper groups.
background
The Yardstick Assignment Principle (Open Problem O1) asks why each particle sector receives a definite $B_{\mathrm{pow}}$ and $r_0$ from the counting layer. Each sector couples to a distinct level of the 3-cube hierarchy; the $r_0$ values are wallpaper-modulated integer offsets built from $W=17$ (Fedorov's count of 2D wallpaper groups).
By definition, $r_0(\mathrm{Lepton})=4W-6=62$ and $r_0(\mathrm{Electroweak})=3W+4=55$. These sit in the mass yardstick $A_s=2^{B_{\mathrm{pow}}}E_{\mathrm{coh}}\varphi^{r_0}$ on the $\varphi$-ladder. Upstream equalities r0_Lepton_eq and r0_Electroweak_eq already pin the two closed forms to 62 and 55 by unfolding $W$ and wallpaper_groups.
proof idea
One-step tactic proof. Unfold the two sector equalities together with the definition of $W$ and wallpaper_groups, then finish by norm_num: $62-55=7$ and $17-10=7$. No intermediate lemmas beyond those two closed forms are required.
why it matters
This is the canonical lepton-versus-EW depth separation in the $r_0$ layer of the O1 table. It makes precise that leptons sit seven rungs above the electroweak sector on the $\varphi$-ladder offset, equal to one wallpaper unit minus ten. The module frames $r_0$ multipliers ${4,2,-1,3}$ as summing to the cube vertex count $V=8$; the present gap is the concrete lepton–EW instance of that wallpaper geometry.
No downstream theorem currently depends on it (used_by is empty), so it functions as a verified structural identity inside the yardstick assignment ledger rather than a stepping stone in a longer chain. It supports the mass-formula story (yardstick $\times\varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$) by locking the relative lepton/EW depth once and for all.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.