r0_alt
plain-language theorem explainer
r0_alt supplies alternative integer expressions for the sector offset r0 in the mass ladder. It is cited by verifications that the first-principles constants match the main Anchor definitions. The definition proceeds by cases on the four sectors, substituting the fixed integers W=17, A=1, E=12 derived from cube geometry and wallpaper groups.
Claim. The alternative sector offset $r_0(s)$ for sector $s$ is given by $r_0($Lepton$)=4W-6$, $r_0($UpQuark$)=2W+A$, $r_0($DownQuark$)=E-W$, $r_0($Electroweak$)=3W+4$, where $W=17$ (wallpaper groups), $A=1$ (active edges per tick), $E=12$ (cube edges in three dimensions).
background
The module verifies sector yardsticks derived from cube combinatorics with $D=3$. Key constants are wallpaper_groups=17, active_edges_per_tick=1, cube_edges($D$)=12. These enter the formulas for $B_{pow}$ and $r_0$ per sector as listed in the module table. Upstream, the Sector inductive type classifies the four sectors (Lepton, UpQuark, DownQuark, Electroweak), while Lepton is defined separately in CrossDomain.CubeFaceUniversality.
proof idea
This is a direct definition by cases on the Sector type. It substitutes the constants Wz, Az, Etz into the listed linear combinations, providing the 8-2 form for the lepton case.
why it matters
This definition feeds the equivalence theorem r0_eq_alt, which confirms that the alternative formulas reproduce the primary Anchor.r0. It closes the verification loop for the parameter-free derivation chain from T8 ($D=3$) and the cube geometry. It supports the mass formula yardstick times phi to the power (rung-8+gap(Z)).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.