anchor_is_unique_valid_r0
plain-language theorem explainer
The anchor $r_0$ sector assignment lies in the filtered set of valid $r_0$ assignments. Cite it when claiming that the yardstick $r_0$ choice is fixed by the structural constraints of the O1 enumeration. The proof rewrites that valid set as a singleton equal to the canonical assignment, then matches the anchor to that canonical form and closes by simplification.
Claim. The anchor $r_0$ assignment belongs to the set of valid $r_0$ assignments obtained by enumerating sector-to-value maps and retaining only those that satisfy the yardstick structural constraints. Under those constraints the valid set is a singleton, so membership is uniqueness of the anchor choice.
background
The module treats the O1 yardstick discussion as a finite combinatorial search. One starts from four candidate $B_{\mathrm{pow}}$ values and four candidate $r_0$ values, enumerates all sector-to-value assignments (permutations), and filters by the structural constraints used in the yardstick principle. The filtered choice sets collapse to singletons for both $B_{\mathrm{pow}}$ and $r_0$.
Sector powers $B_{\mathrm{pow}}$ are not free parameters: they are the derived powers of two attached to Lepton, UpQuark, DownQuark, and Electroweak from cube edge counting (Anchor). The $r_0$ side of the same enumeration is the object here: anchorR0Assignment is the concrete anchor map, and validR0Assignments is the filtered list/set of maps that survive the principle constraints.
Upstream, the proof depends on the local facts that the valid $r_0$ list is a singleton and that the anchor map matches the canonical survivor of that filter.
proof idea
Short tactic proof. Rewrite the membership goal with two local lemmas: the valid $r_0$ assignment set is a singleton, and the anchor $r_0$ assignment equals the canonical element of that singleton. After those rewrites, simp discharges the residual list/set membership goal. No external arithmetic or forcing lemmas are invoked in the body; the work is pure equality and singleton membership.
why it matters
In Recognition Science the mass formula is yardstick times a $\varphi$-ladder factor $\varphi^{(\mathrm{rung}-8+\mathrm{gap}(Z))}$. Fixing the yardstick assignment (including the $r_0$ sector map) is therefore a verification gate before mass numerics can be treated as forced rather than fitted.
This theorem records that the anchor $r_0$ map is not merely a preferred convention: it is the unique survivor of the O1 structural filter. The module doc states that both $B_{\mathrm{pow}}$ and $r_0$ valid choice sets collapse to singletons; this declaration is the $r_0$ half of that collapse at the level of membership.
No downstream consumers are wired in the graph yet (used_by is empty). The natural landing sites are later uniqueness or export theorems that quote a single canonical $r_0$ assignment when assembling the full yardstick package.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.