validR0Assignments
plain-language theorem explainer
The finite list of sector-to-integer r0 assignments that survive the structural yardstick filters (sign and ordering of down/lepton/ew/up plus the fixed sum target). Anyone proving uniqueness of the canonical r0 anchor or the O1 choice-set collapse cites this list. It is a one-line filter of the full permutation pool by the boolean structural predicate.
Claim. Let an $r_0$ assignment be a 4-tuple of integers $(r_\ell, r_u, r_d, r_{\mathrm{ew}})$ for the lepton, up, down, and electroweak sectors. The valid $r_0$ assignments are exactly those permutations of the candidate $r_0$ value pool that satisfy $r_d < 0$, $r_\ell > r_{\mathrm{ew}} > r_u$, and $r_\ell + r_u + r_d + r_{\mathrm{ew}} = V W + E_{\mathrm{passive}}$ (the structural sum target).
background
This module turns the O1 yardstick discussion into an explicit finite search. One starts from four candidate $r_0$ values, forms every sector-to-value assignment (all permutations of the pool), and retains only those that meet the structural constraints used in the yardstick argument. The same pattern is run in parallel for $B_{\mathrm{pow}}$.
An $r_0$ assignment is a record of four integers, one per sector (lepton, up, down, electroweak). The full candidate list is the image of the $r_0$ value-pool permutations under the list-to-assignment map. Structural filtering requires a negative down entry, the strict ordering lepton $>$ electroweak $>$ up, and equality of the four-sector sum to the fixed target $VW + E_{\mathrm{passive}}$ (documented as 147 in the sum-target comment).
The module claim is that, after these filters, both the $B_{\mathrm{pow}}$ and $r_0$ valid sets collapse to singletons.
proof idea
Pure definition: take the exhaustive list of $r_0$ assignments obtained from permutations of the value pool, and retain only those for which the boolean structural predicate returns true. No tactic proof; the body is a single List.filter of that predicate over the full assignment list.
why it matters
This list is the object whose cardinality and contents the uniqueness theorems inspect. Downstream, valid_r0_assignment_count and valid_r0_assignments_are_singleton show by native decision that the list equals the singleton containing the canonical $r_0$ assignment. That singleton fact is the $r_0$ half of yardstick_choice_sets_collapsed, the O1 enumerated-choice closure summary.
It also feeds the forcing argument: any assignment already in the full pool that satisfies the principle-level constraints is shown to lie in this filtered list and therefore equal the canonical anchor. Membership of the anchor itself is recorded separately. In the broader Recognition picture this is verification scaffolding for the mass-yardstick side of the $\varphi$-ladder (rung offsets relative to the eight-tick baseline), not a new forcing step in T0–T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.