all_bpow_assignments_count
plain-language theorem explainer
The raw list of sector-to-B_pow assignments built by permuting the four-candidate value pool has exactly 24 entries. Anyone auditing the O1 yardstick choice-set search cites this as the unfiltered combinatorial size (4!). The proof is a one-line native_decide on that concrete list.
Claim. The list of all $B_{\mathrm{pow}}$ sector assignments obtained by taking every permutation of the four-candidate $B_{\mathrm{pow}}$ value pool and converting each permutation into an assignment has length $24$.
background
The module turns the O1 yardstick discussion into 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 by permuting the pool, then filters by the structural constraints used in the yardstick argument. Under those filters the surviving choice sets collapse to singletons for both $B_{\mathrm{pow}}$ and $r_0$.
Here allBPowAssignments is exactly the unfiltered list: permutations of bPowValuePool, each turned into a BPowAssignment via listToBPowAssignment?. With four distinct pool entries one expects $4! = 24$ permutations; this theorem records that count. In the broader RS mass story the yardstick multiplies the $\varphi$-ladder term $\varphi^{(\mathrm{rung}-8+\mathrm{gap}(Z))}$, so fixing which sector receives which $B_{\mathrm{pow}}$ is part of locking the absolute mass scale.
proof idea
One-line wrapper: native_decide evaluates the concrete List.length of allBPowAssignments in the kernel and closes the equality to 24. No lemmas beyond the definition of that list and ordinary list length are required.
why it matters
This is bookkeeping for the O1 yardstick assignment program: before structural and principle constraints are applied, the search space size must be known and machine-checked. The module goal is that those constraints collapse the valid $B_{\mathrm{pow}}$ (and $r_0$) choice sets to singletons, which is the combinatorial side of selecting the unique yardstick that feeds the RS mass formula. No downstream theorem currently depends on the count, but every later filter proof sits on top of this enumerated pool. It does not itself invoke T5–T8 or the RCL; it only sizes the discrete assignment space those later uniqueness claims act on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.