validBPowAssignments
plain-language theorem explainer
The finite list of sector-to-integer B_pow assignments that survive the structural yardstick filters. Anyone checking O1 uniqueness of the mass-ladder yardstick cites this set: it is the search space after discarding permutations that violate pairing, positivity, and sum-to-one. Defined by filtering the full permutation pool with those Boolean constraints.
Claim. Let a $B_{\mathrm{pow}}$ assignment be a 4-tuple of integers $(B_\ell, B_u, B_d, B_{\mathrm{ew}})$ for the lepton, up, down, and electroweak sectors. The valid $B_{\mathrm{pow}}$ assignments are those permutations of the candidate value pool that satisfy: $B_u = -B_{\mathrm{ew}}$, $|B_\ell| + |B_{\mathrm{ew}}| = B_d$, $B_u < 0$, $B_{\mathrm{ew}} > 0$, and $B_\ell + B_u + B_d + B_{\mathrm{ew}} = 1$.
background
The module treats O1 yardstick assignment as a finite combinatorial search. Four candidate integer powers for $B_{\mathrm{pow}}$ and four for $r_0$ are fixed; every sector-to-value assignment is a permutation of the corresponding pool. A $B_{\mathrm{pow}}$ assignment is a structure with integer fields for lepton, up, down, and electroweak sectors.
The full candidate list is every permutation of the $B_{\mathrm{pow}}$ value pool that successfully packs into such a 4-tuple. Structural filters then enforce the pairing and sum relations used in the yardstick discussion: opposite up/EW powers, absolute-value relation for the down power, sign conditions, and total sum equal to the structural target $A = 1$.
Under those constraints the surviving choice sets are claimed to collapse to singletons for both $B_{\mathrm{pow}}$ and $r_0$.
proof idea
One-line definitional filter: take the exhaustive list of packed permutations of the $B_{\mathrm{pow}}$ value pool and retain only those entries for which the structural Boolean predicate returns true. No tactic proof; the body is filter applied to that predicate.
why it matters
This is the concrete choice set whose cardinality and contents close the O1 enumeration for $B_{\mathrm{pow}}$. Downstream, native decision shows the list has length one and equals the singleton of the canonical assignment; the joint collapse theorem packages that with the matching $r_0$ result. Forcing lemmas use membership in this filtered list to conclude any principle-satisfying assignment equals the canonical one, and the anchor assignment is proved to lie in it.
In the broader Recognition picture this pins the sector exponents that enter the mass yardstick on the $\varphi$-ladder (masses as yardstick times $\varphi$ to a rung-shifted power). Collapsing the combinatorial freedom is the verification step that the yardstick is not an arbitrary labeling among permutations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.