r0_formula_identities
plain-language theorem explainer
Four closed-form identities write each sector's r₀ offset as an integer linear form in the counting-layer constants W, A, and E_total. Anyone auditing the yardstick table against the 3-cube hierarchy cites this. The proof is pure definitional simplification of the sector-wise r₀ map.
Claim. With counting-layer integers $W$ (wallpaper count), $A$ (active-edge count), and $E_{\mathrm{total}}$ (total-edge count), the sector offsets satisfy $r_0(\mathrm{Lepton})=4W-6$, $r_0(\mathrm{Up\ quark})=2W+A$, $r_0(\mathrm{Down\ quark})=E_{\mathrm{total}}-W$, and $r_0(\mathrm{Electroweak})=3W+4$.
background
The Yardstick Assignment Principle module treats Open Problem O1: why each particle sector receives a definite $B_{\mathrm{pow}}$ and $r_0$ formula from the counting layer of the 3-cube. Sectors couple to distinct levels of that hierarchy (passive edges, active edge, total edges), and the yardstick formulas encode the coupling.
Here $r_0$ is the wallpaper-modulated integer offset on the $\varphi$-ladder mass formula. The counting constants are $W=17$ (wallpaper groups), $A=1$ (active edges per tick, from the gap-derivation layer), and $E_{\mathrm{total}}$ (total edge count of the cube network). Numerically the table reads $4W-6=62$, $2W+A=35$, $E-W=-5$, $3W+4=55$.
The $W$-multipliers ${4,2,-1,3}$ sum to $8=V$, the vertex count of the cube; that structural sum is recorded by the sibling identity equating $\sum r_0$ to $V\cdot W+E_{\mathrm{passive}}$.
proof idea
Term-mode proof built from four constructor steps, one conjunct each. Every branch is a single simp [r0]: the sector-indexed definition of $r_0$ unfolds definitionally to the stated linear form in $W$, $A$, or $E_{\mathrm{total}}$. No external lemmas are required beyond the definition of $r_0$ and the integer casts of the counting constants.
why it matters
This is the formula-level half of the $r_0$ column in the O1 yardstick table. It pins the four sector offsets to counting-layer constants rather than ad-hoc integers, so later numerical checks ($r_0$ values, the sum identity $\sum r_0=V\cdot W+E_{\mathrm{passive}}=147$) rest on algebra, not table lookup.
In the Recognition framework the offsets sit on the $\varphi$-ladder mass formula (yardstick $\cdot\varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$). The $W$-multipliers summing to $V=8$ ties the offsets to the eight-tick octave and the $D=3$ cube combinatorics (forcing chain T7–T8). Downstream siblings use these identities to prove the global sum; the declaration itself has no further used_by edges yet, but it closes the formula side of O1 for $r_0$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.