valid_bpow_assignments_are_singleton
plain-language theorem explainer
Under the structural yardstick constraints, the finite list of sector-to-B_pow assignments collapses to exactly one entry: the canonical assignment. Anyone proving uniqueness of the B_pow sector map in the O1 enumeration cites this equality. The proof is a one-line native_decide over the filtered finite search space.
Claim. The list of $B_{\mathrm{pow}}$ sector assignments that pass the structural constraints equals the singleton list whose only element is the canonical assignment (lepton $\mapsto -2E_{\mathrm{passive}}$, up $\mapsto -A$, down $\mapsto 2E_{\mathrm{total}}-1$, electroweak $\mapsto A$).
background
This module turns the O1 yardstick discussion into an explicit finite combinatorial search. One starts from four candidate $B_{\mathrm{pow}}$ values and enumerates all sector-to-value assignments (permutations across lepton, up, down, and electroweak sectors), then filters by the structural constraints used in the yardstick principle.
The canonical assignment is the concrete map lepton $\mapsto -2E_{\mathrm{passive}}$, up $\mapsto -A$, down $\mapsto 2E_{\mathrm{total}}-1$, electroweak $\mapsto A$. The valid list is defined as the full assignment pool filtered by those structural constraints. The module claim is that both the $B_{\mathrm{pow}}$ and $r_0$ valid choice sets collapse to singletons under the current constraint set.
proof idea
One-line wrapper that applies native_decide. Because validBPowAssignments is a concrete finite list obtained by filtering a finite enumeration, equality to the singleton [canonicalBPow] is a decidable proposition on closed terms and is discharged by computation.
why it matters
This is the $B_{\mathrm{pow}}$ half of the O1 enumerated-choice closure. Downstream, yardstick_choice_sets_collapsed packages it with the matching $r_0$ singleton result as the joint summary that both valid choice sets collapse. It also feeds bpow_constraints_force_canonical (any assignment in the full pool that meets the principle constraints must equal the canonical one) and anchor_is_unique_valid_bpow (the anchor assignment lies in the valid list, via rewrite along this equality).
In the broader Recognition framework this is verification scaffolding for the mass yardstick on the phi-ladder: once sector $B_{\mathrm{pow}}$ values are forced, the rung-to-mass map has a unique combinatorial seed rather than a free choice among permutations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.