BPowAssignment
plain-language theorem explainer
A B-power assignment is a four-tuple of integers, one exponent per sector (lepton, up quark, down quark, electroweak). Anyone enumerating or filtering yardstick B_pow choices cites this carrier type. It is a plain structure with decidable equality; no proof content.
Claim. A $B$-power assignment is a 4-tuple $(B_\ell, B_u, B_d, B_{\mathrm{EW}}) \in \mathbb{Z}^4$ of integer exponents attached to the lepton, up-quark, down-quark, and electroweak sectors respectively.
background
The module treats the O1 yardstick discussion as a finite combinatorial search: four candidate $B_{\mathrm{pow}}$ values are permuted across four sectors, then filtered by structural constraints from the yardstick principle. Valid filtered sets collapse to a singleton.
In Recognition Science the mass formula uses a yardstick times a $\varphi$-ladder power whose sector-dependent exponent is this $B_{\mathrm{pow}}$. The four fields of the structure are exactly those sector labels. Sibling definitions supply the candidate pool, the sum target $A=1$, and boolean structural/principle filters.
The import of Anchor and YardstickAssignmentPrinciple supplies the sector-indexed $B_{\mathrm{pow}}$ formulas and the constraint language used later; the cosmology up/down species names are only name collisions, not physical inputs here.
proof idea
No proof: this is a structure declaration with four integer fields and derived Repr and DecidableEq. Downstream code builds values by field update or by listToBPowAssignment? on permutations of the value pool.
why it matters
This is the carrier type for the entire $B_{\mathrm{pow}}$ choice-set pipeline. allBPowAssignments enumerates every sector-to-value permutation; anchorBPowAssignment records the canonical Anchor formulas; and the boolean constraint theorems (bpow_bool_constraints_forced_from_edge_roles, passive/active role variants, and the iff forms that force $|B_{\mathrm{EW}}|=A$) all quantify over this type.
Those filters are what make the O1 claim precise: under structural sum and edge-role hypotheses the admissible set collapses to one assignment. That uniqueness is the combinatorial half of fixing the yardstick exponents that enter the $\varphi$-ladder mass formula. It does not itself derive the mass spectrum; it packages the discrete choice that later uniqueness theorems pin down.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.