canonicalBPow
plain-language theorem explainer
The canonical four-sector B_pow assignment: lepton −2E_passive, up −A, down 2E_total−1, electroweak +A. With the cube-edge anchors this is (−22, −1, 23, +1). Every forcing theorem in the yardstick choice-set module cites it as the unique survivor under structural and principle constraints. The body is a pure structure literal, no proof.
Claim. The canonical $B_{\mathrm{pow}}$ assignment on the four sectors is the integer 4-tuple $\bigl(\ell,u,d,w\bigr)=\bigl(-2E_{\mathrm{passive}},\,-A,\,2E_{\mathrm{total}}-1,\,A\bigr)$, where $E_{\mathrm{passive}}$ is the passive edge count, $E_{\mathrm{total}}$ the total cube-edge count, and $A$ the active-edge count per tick.
background
The module treats O1 yardstick assignment as a finite combinatorial search: four candidate $B_{\mathrm{pow}}$ values are permuted across the lepton, up, down, and electroweak sectors, then filtered by structural and principle constraints. The ambient type is BPowAssignment, a plain record of four integers, one per sector.
The numeric anchors come from the mass/geometry layer. Total cube edges are $E_{\mathrm{total}}=12$; passive field edges are $E_{\mathrm{passive}}=11$; active edges per tick are $A=1$. These are the same edge counts that feed the mass ladder and the gap derivation ($\eta_B\cdot\Theta_{\mathrm{crit}}=\varphi^A$).
The mirrored counterpart flips only the active-edge sign pattern, so the choice set is a genuine two-branch orientation problem before positivity of the electroweak entry selects one side.
proof idea
Definitional structure literal. Each field is an integer expression in the anchor constants $E_{\mathrm{passive}}$, $E_{\mathrm{total}}$, and $A$, cast to $\mathbb{Z}$. No tactics, no lemmas, no computation beyond the casts.
why it matters
This is the reference point for the entire B_pow forcing chain in the yardstick verification module. Downstream theorems such as bpow_constraints_force_canonical, bpow_unrestricted_forcing_from_down_role, and the orientation selectors prove that every assignment surviving the principle constraints equals this tuple. The two-branch lemma isolates exactly this assignment and its mirror; positive electroweak orientation then kills the mirror.
In the broader RS picture the exponents sit on the $\varphi$-ladder mass formula (yardstick times $\varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$). Fixing the sector powers is the combinatorial half of locking the yardstick, which is why the module frames the work as O1 progress: the valid choice set collapses to a singleton once structural sum, sign duality, and active-unit magnitude are imposed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.