r0_pool_matches_anchor_formulas
plain-language theorem explainer
The four-element candidate pool of integer r0 offsets is definitionally the same list as the sector-wise anchor formulas for lepton, up-quark, down-quark, and electroweak. Anyone auditing the yardstick choice-set enumeration against the mass-anchor definitions would cite this equality. The proof is a one-line reflexivity check.
Claim. The ordered candidate pool of $r_0$ values equals $[r_0(\mathrm{Lepton}),\, r_0(\mathrm{UpQuark}),\, r_0(\mathrm{DownQuark}),\, r_0(\mathrm{Electroweak})]$, where each $r_0$ is the derived $\varphi$-exponent offset for that sector coming from wallpaper and cube geometry.
background
In the mass-anchor layer, each sector carries a fixed integer offset $r_0$ on the $\varphi$-ladder. These offsets are not free parameters: the lepton, up-quark, down-quark, and electroweak cases are written as $4W-6$, $2W+A$, $E_{\mathrm{total}}-W$, and $3W+4$ respectively, with the integers $W$, $A$, and $E_{\mathrm{total}}$ fixed by wallpaper and cube geometry.
This module turns the O1 yardstick discussion into a finite combinatorial search. It begins with four candidate $B_{\mathrm{pow}}$ values and four candidate $r_0$ values, enumerates all sector-to-value assignments, and filters by the structural constraints used in the yardstick principle. The $r_0$ candidate list is exactly the four closed-form expressions above, written as a bare integer list rather than as applications of the sector map.
The present statement simply identifies that bare list with the image of the four sectors under the anchor map $r_0$.
proof idea
One-line reflexivity. Unfolding the pool definition yields the four arithmetic expressions $4W-6$, $2W+A$, $E_{\mathrm{total}}-W$, $3W+4$. Unfolding $r_0$ on the four sector constructors yields the same four expressions in the same order. Definitional equality closes the goal with rfl; no lemmas are invoked.
why it matters
The yardstick assignment program needs a single, auditable source of truth for the four $r_0$ candidates before it enumerates permutations and applies structural filters. This equality pins the combinatorial pool to the geometric anchor formulas, so any later uniqueness claim about the surviving $r_0$ assignment is talking about the same integers that the mass ladder uses.
In the broader Recognition framework those offsets sit inside the mass formula (yardstick times $\varphi$ to a rung shifted by $r_0$ and a charge gap). The module doc records that, once structural constraints are imposed, both the $B_{\mathrm{pow}}$ and $r_0$ choice sets collapse to singletons; this lemma is the $r_0$ side of the bookkeeping that makes that collapse well-defined. No downstream theorem currently depends on it, but it is the natural rewrite bridge between the anchor module and the choice-set filters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.