valid_r0_assignment_count
plain-language theorem explainer
Exactly one sector-to-value map for the four candidate $r_0$ yardstick parameters survives the structural filters used in the O1 yardstick discussion. Anyone checking uniqueness of the $r_0$ assignment in the finite choice-set enumeration would cite this. The proof is a one-line `native_decide` on the concrete filtered list.
Claim. The finite list of $r_0$ sector assignments that pass the yardstick structural constraints has cardinality $1$: there is a unique valid $r_0$ assignment under those filters.
background
The module treats the O1 yardstick discussion as a finite combinatorial search. One starts from four candidate $r_0$ values and all sector-to-value assignments (permutations), then retains only those maps that satisfy the structural constraints used in the yardstick principle.
validR0Assignments is exactly that filtered list: every candidate assignment from the full enumeration, kept only if it meets r0StructuralConstraints. The same pattern is run in parallel for the $B_{\mathrm{pow}}$ pool; the module claims both filtered choice sets collapse to singletons.
The local setting is verification of uniqueness by exhaustive enumeration, not an analytic fixed-point argument. List length here is ordinary finite cardinality of the surviving assignment list.
proof idea
One-line wrapper: native_decide evaluates the concrete List definition of the filtered $r_0$ assignments and checks that its length equals one. No intermediate lemmas are invoked beyond the definition of the filtered list itself.
why it matters
This pins the O1 claim that the $r_0$ yardstick choice set is a singleton once structural constraints are imposed. Together with the parallel $B_{\mathrm{pow}}$ count, it turns the yardstick assignment discussion into an explicit finite uniqueness statement rather than an informal selection among candidates.
In the broader Recognition framework the yardstick feeds the mass ladder (yardstick times $\varphi$ raised to rung offsets). Unique $r_0$ assignment removes a discrete ambiguity before those mass formulas are used. No downstream theorems currently depend on this declaration in the graph; it stands as a terminal verification fact for the $r_0$ side of the choice-set enumeration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.