allBPowAssignments
plain-language theorem explainer
Enumerates every bijection from the four particle sectors to the four cube-edge-derived B-power integers. Verification lemmas cite it as the finite search space whose structural filters collapse to the single canonical yardstick. The body is a one-line list comprehension: all permutations of the fixed value pool, packed into assignment records.
Claim. Let the candidate pool be the four integers $\{-2E_{\mathrm{passive}}, -A, 2E_{\mathrm{total}}-1, A\}$ coming from cube-edge counting. The full assignment list is every permutation of that pool, each interpreted as a 4-tuple $(\mathrm{lepton},\mathrm{up},\mathrm{down},\mathrm{ew})$ of sector powers.
background
The module turns the O1 yardstick discussion into a finite combinatorial search: four candidate $B_{\mathrm{pow}}$ values and four sectors, enumerate all sector-to-value maps, then filter by structural constraints. The resulting valid sets are claimed to collapse to singletons.
$B_{\mathrm{pow}}$ itself is not free. Anchor derives it from cube edge counting: lepton $-2E_{\mathrm{passive}}=-22$, up $-A=-1$, down $2E_{\mathrm{total}}-1=23$, electroweak $+A=+1$, with active edges per tick $A=1$. The local pool bPowValuePool is exactly those four integers unordered.
An assignment record is a 4-tuple of integers, one per sector (lepton, up, down, electroweak). Converting a length-4 list into such a record is the only packing step; other lengths are discarded.
proof idea
Pure definition, not a proof. Take every permutation of the four-element candidate pool, then filterMap through the partial packer that accepts only length-4 lists and builds the sector record. The result is the exhaustive list of bijections from sectors to the fixed multiset of powers (here a set of four distinct values, so $4!=24$ entries).
why it matters
This list is the raw choice set for O1 progress on yardstick uniqueness. Downstream, validBPowAssignments filters it by structural constraints; all_bpow_assignments_count certifies length 24 by native decision; and bpow_constraints_force_canonical shows every member satisfying the principle constraints equals the canonical cube-edge assignment.
In the broader RS picture the powers feed the mass ladder (yardstick times $\varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$). Forcing the sector powers by enumeration-plus-constraints, rather than by fiat, closes a verification gap between Anchor's geometric formulas and the unique physical labeling of lepton, quark, and electroweak sectors.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.