anchorBPowAssignment
plain-language theorem explainer
Packages the four sector powers from the mass-anchor formulas into one assignment record (lepton, up, down, electroweak). Verification and uniqueness proofs cite it as the concrete candidate against which the finite B_pow choice set is filtered. The body is a pure structure literal wiring each field to the corresponding B_pow sector value.
Claim. Define the anchor $B$-power assignment by $B_{\ell}=B_{\mathrm{pow}}(\mathrm{Lepton})$, $B_{u}=B_{\mathrm{pow}}(\mathrm{Up})$, $B_{d}=B_{\mathrm{pow}}(\mathrm{Down})$, $B_{\mathrm{EW}}=B_{\mathrm{pow}}(\mathrm{EW})$, i.e. the integers $(-22,-1,23,1)$ coming from cube-edge counting.
background
The module treats O1 yardstick assignment as a finite combinatorial search: take the four candidate $B_{\mathrm{pow}}$ integers, assign them to the four sectors (all permutations), and keep only those records that pass the structural filters used in the yardstick discussion. Valid choice sets collapse to singletons.
BPowAssignment is the plain four-field integer record (lepton, up, down, electroweak). Upstream, B_pow on Sector is not free: "These are NOT arbitrary—they come from cube edge counting," with values lepton $-(2E_{\mathrm{passive}})=-22$, up $-A=-1$, down $2E_{\mathrm{total}}-1=23$, electroweak $A=1$.
This definition is the bridge from Masses.Anchor into the choice-set layer: it is the anchor-derived point inside the enumerated pool.
proof idea
Definitional structure literal, not a proof. Each field of BPowAssignment is set by applying the sector map B_pow to the matching constructor (Lepton, UpQuark, DownQuark, Electroweak). No tactics or lemmas; equality to the canonical pool element is discharged later by native_decide.
why it matters
Gives the choice-set machinery a named anchor point so uniqueness can be stated as membership rather than as an abstract formula. Downstream: anchor_bpow_matches_canonical equates it to canonicalBPow; anchor_is_unique_valid_bpow places it in validBPowAssignments via the singleton theorem; anchor_bpow_structural_identities and anchor_bpow_constraints_from_principle show the structural filter holds, each conjunct matching a proved identity from YardstickAssignmentPrinciple.
In the broader RS mass story the $B_{\mathrm{pow}}$ integers fix the sector exponents on the $\varphi$-ladder (mass yardstick $\cdot,\varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$). Closing the O1 enumeration to a singleton for $B_{\mathrm{pow}}$ is the combinatorial half of forcing those exponents rather than fitting them.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.