valid_r0_assignments_are_singleton
plain-language theorem explainer
The filtered list of valid sector-to-r0 assignments equals the singleton containing only the canonical assignment. Citation target for O1 yardstick uniqueness and the joint collapsed choice-set theorem. Proof is a one-line native computational decision on the finite filtered enumeration.
Claim. The list of $r_0$ assignments obtained by filtering all sector-to-value permutations against the structural constraints equals the singleton list whose sole element is the canonical assignment: lepton $4W-6$, up $2W+A$, down $E_{\mathrm{total}}-W$, electroweak $3W+4$.
background
This module turns the O1 yardstick discussion into a finite combinatorial search. Four candidate $r_0$ values are assigned to the four sectors (lepton, up, down, electroweak) by enumerating all permutations, then retained only if they pass the structural constraints used in the yardstick principle.
The canonical assignment is the concrete record lepton $\mapsto 4W-6$, up $\mapsto 2W+A$, down $\mapsto E_{\mathrm{total}}-W$, electroweak $\mapsto 3W+4$. The valid list is defined as that full permutation pool filtered by the structural predicate. The module's stated goal is that both the $B_{\mathrm{pow}}$ and $r_0$ valid sets collapse to singletons under the current constraint set.
proof idea
One-line wrapper: native_decide decides equality of two concrete finite lists by computation. The left side is the filtered enumeration of all $r_0$ assignments under the structural constraints; the right side is the singleton list of the hard-coded canonical record. No algebraic lemmas are applied beyond decidable equality on the enumerated data.
why it matters
Feeds three parents: the forcing theorem that any pool member satisfying the principle constraints equals the canonical assignment; the membership proof that the anchor assignment lies in the valid list; and the joint O1 closure summary that both valid $B_{\mathrm{pow}}$ and valid $r_0$ choice sets are singletons. That joint theorem is the enumerated-choice closure for O1 under the current constraint set. In Recognition Science this is verification scaffolding for the mass-ladder yardstick (the rung offset in the $\varphi$-ladder mass formula), not a step of the T0--T8 forcing chain itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.