r0ValuePool
plain-language theorem explainer
Four integer candidates for the sector yardstick offsets r0, written in closed form from the anchor constants W, A, and E_total. Anyone enumerating sector-to-rung assignments cites this pool as the raw choice set before permutation and filtering. The body is a four-element list literal; no proof.
Claim. The candidate pool for sector offsets $r_0$ is the four-element integer list $$\bigl[4W-6,\; 2W+A,\; E_{\mathrm{total}}-W,\; 3W+4\bigr],$$ where $W$ is the wallpaper-group count, $A$ the active-edge count per tick, and $E_{\mathrm{total}}$ the total cube-edge count.
background
The module treats the O1 yardstick discussion as a finite combinatorial search: four candidate $B_{\mathrm{pow}}$ values and four candidate $r_0$ values are assigned to the four mass sectors (lepton, up-quark, down-quark, electroweak) by permutation, then filtered by structural constraints. Valid choice sets collapse to singletons under those constraints.
The anchor constants used here are the standard RS mass-topology integers: wallpaper groups $W=17$, active edges per tick $A=1$, and total cube edges $E_{\mathrm{total}}=12$ (the $Q_3$ edge count). Each list entry is the closed-form expression that the sector-wise $r_0$ formula evaluates to on those anchors.
Downstream, a reflexivity check records that the four expressions equal the sector formulas $r_0(\mathrm{Lepton})$, $r_0(\mathrm{UpQuark})$, $r_0(\mathrm{DownQuark})$, $r_0(\mathrm{Electroweak})$ in that order.
proof idea
Pure definition: a four-element List ℤ literal. Each entry is an integer linear form in the anchor abbreviations W, A, and E_total, cast to ℤ. No tactics, no lemmas.
why it matters
This pool is the raw input to the r0 half of the O1 choice-set enumeration. allR0Assignments takes all permutations of the pool and converts them into sector assignments; structural and principle filters then collapse the valid sets to a singleton. The companion theorem r0_pool_matches_anchor_formulas pins the list order to the four sector formulas by rfl, so the combinatorial search is literally searching over the anchor-derived rung offsets rather than an ad-hoc integer set.
In the broader RS mass ladder, $r_0$ shifts the rung index in the yardstick formula (mass $\propto \varphi^{r-8+\mathrm{gap}(Z)}$). Fixing the four sector offsets by exhaustive constrained search is the verification step that the yardstick assignment is forced, not chosen.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.