valid_bpow_assignment_count
plain-language theorem explainer
Under the yardstick structural filters, exactly one sector-to-value assignment of the four candidate B_pow constants survives. Anyone citing uniqueness of the RS mass-yardstick assignment (O1) needs this count. The proof is a one-line native decision on a finite filtered list.
Claim. The filtered list of valid $B_{\mathrm{pow}}$ sector assignments has length $1$: after enumerating all assignments of the four candidate $B_{\mathrm{pow}}$ values to sectors and retaining only those that satisfy the structural yardstick constraints, exactly one assignment remains.
background
The module treats the O1 yardstick discussion as a finite combinatorial search. One starts from four candidate $B_{\mathrm{pow}}$ values (and, separately, four candidate $r_0$ values), forms every sector-to-value assignment, and keeps only those that meet the structural constraints used in the yardstick argument. The module claim is that both filtered choice sets collapse to singletons.
Here the object of study is the $B_{\mathrm{pow}}$ side. All assignments are generated, then filtered by the structural predicate; the surviving list is the valid $B_{\mathrm{pow}}$ assignment set. Length is ordinary finite-list length (as in the primitive trace-length definition: empty has length $0$, each extension adds one).
The companion facts in the module pin the pool to the anchor formulas and match the sum target to the yardstick principle, so the filter is not an ad hoc cut: it encodes the same structural and principle constraints already used in the yardstick assignment discussion.
proof idea
One-line wrapper: native_decide evaluates the closed finite computation validBPowAssignments.length = 1 at compile time. The list itself is defined by filtering the full assignment enumeration through the structural constraint predicate, so the decision procedure simply counts the survivors. No algebraic rewriting or external lemma application is required beyond that definitional unfolding.
why it matters
Recognition Science fixes particle masses on a $\varphi$-ladder with a yardstick prefactor; which sector receives which $B_{\mathrm{pow}}$ is part of that assignment story. This count makes the O1 uniqueness claim fully explicit: the structural filter leaves a singleton, so the $B_{\mathrm{pow}}$ sector map is combinatorially forced rather than chosen by hand.
No downstream theorem currently depends on this declaration in the graph, so it functions as a verification endpoint for the choice-set module rather than a lemma inside a longer proof chain. It sits next to the matching $r_0$ enumeration and the pool/anchor consistency facts, closing the "how many valid yardstick assignments?" question for $B_{\mathrm{pow}}$ under the stated constraints. Framework-wise it supports the mass-formula side (yardstick $\times \varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$) by pinning the discrete prefactor assignment.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.