bpow_constraints_force_canonical
plain-language theorem explainer
Any integer B_pow assignment to the four sectors (lepton, up, down, electroweak) that sits in the enumerated candidate pool and meets the Yardstick principle constraints equals the canonical assignment. Yardstick and mass-ladder verification cite this uniqueness. The proof converts principle constraints to structural ones, filters the pool, and applies a prior singleton lemma.
Claim. Let $a$ be an assignment of integer $B_{\mathrm{pow}}$ values to the lepton, up, down, and electroweak sectors. If $a$ lies in the finite set of all sector-to-value assignments drawn from the candidate pool, and if $a$ satisfies the Yardstick principle constraints on $B_{\mathrm{pow}}$, then $a$ equals the canonical $B_{\mathrm{pow}}$ assignment.
background
Recognition Science mass formulas place species on a $\varphi$-ladder scaled by a yardstick. The O1 discussion asks which integer $B_{\mathrm{pow}}$ values attach to the four sectors lepton, up, down, and electroweak. This module turns that into a finite combinatorial search: four candidate $B_{\mathrm{pow}}$ values, all sector-to-value assignments (permutations), then a filter by structural constraints from the Yardstick discussion. The module header states that valid choice sets collapse to singletons for both $B_{\mathrm{pow}}$ and $r_0$.
An assignment is a 4-tuple of integers $(B_\ell,B_u,B_d,B_{\mathrm{ew}})$. Principle constraints package the physical requirements used in the yardstick argument (sum targets, active-edge pairing, sign conditions). Structural constraints are the Boolean form of those same filters. A companion remark records the forced normal form: active-edge pair fixed ($B_{\mathrm{ew}}=1$, $B_u=-1$), down value $1-B_\ell$, and lepton nonpositive.
proof idea
Apply the equivalence between principle and structural constraints to obtain the Boolean structural flag true. Unfold the filtered list of valid assignments and package pool membership with that flag, so the assignment lies in the valid list. Rewrite with the prior singleton lemma asserting that the valid list is exactly ${\mathrm{canonical}}$, then simplify to equality with the canonical assignment.
why it matters
This is the uniqueness half of the O1 yardstick enumeration for $B_{\mathrm{pow}}$: once principle constraints are imposed, the combinatorial search leaves no residual freedom. That fixed assignment is what mass-ladder and anchor verification need before rung formulas and gap corrections can run. The module frames the whole development as making the O1 choice-set discussion explicit and showing collapse to a singleton. No downstream edges are wired yet; the lemma is a terminal verification step for the claimed choice-set collapse. Framework context is the $\varphi$-ladder mass formula (yardstick times $\varphi$ to a rung offset), not the T0–T8 forcing chain itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.