bpow_unrestricted_forcing_from_edge_roles
plain-language theorem explainer
Any integer B-power assignment to the lepton, up, down, and electroweak sectors that obeys the edge-role identities (down fixed by total edge count, up opposite electroweak, electroweak positive of magnitude A, four exponents summing to the target) equals the canonical assignment. Yardstick and mass-ladder verifiers cite this to replace finite enumeration by algebraic forcing. The proof derives principle constraints from the edge roles, then applies unrestricted down-role forcing.
Claim. Let $a$ assign integer $B_{\mathrm{pow}}$ exponents to the four sectors (lepton, up, down, electroweak). If $a_{\mathrm{down}}=2E_{\mathrm{total}}-1$, $a_{\mathrm{up}}=-a_{\mathrm{ew}}$, $a_{\mathrm{ew}}>0$, $|a_{\mathrm{ew}}|=A$ (active-edge count per tick), and $a_{\mathrm{lepton}}+a_{\mathrm{up}}+a_{\mathrm{down}}+a_{\mathrm{ew}}$ equals the $B_{\mathrm{pow}}$ sum target, then $a$ equals the canonical $B_{\mathrm{pow}}$ assignment.
background
The module treats O1 yardstick assignment as a finite combinatorial search: four candidate $B_{\mathrm{pow}}$ values and four candidate $r_0$ values, all sector-to-value permutations, filtered by structural constraints from the Yardstick discussion. Valid choice sets collapse to singletons for both $B_{\mathrm{pow}}$ and $r_0$.
A $B_{\mathrm{pow}}$ assignment is a 4-tuple of integers $(a_{\mathrm{lepton}},a_{\mathrm{up}},a_{\mathrm{down}},a_{\mathrm{ew}})$. The constant $A$ is the active-edge count per tick ($A=1$ in the gap derivation). The sum target is the fixed integer that the four sector exponents must add to under the yardstick principle (sibling facts record that this target equals one and matches the principle form).
Edge roles encode structural identities: the down exponent is pinned by total edge count as $2E_{\mathrm{total}}-1$; the up and electroweak exponents are opposite in sign; electroweak is the positive active edge of magnitude $A$. This theorem lifts those role assumptions to full canonical uniqueness without enumerating the assignment pool.
proof idea
Two-step term proof. First apply the lemma that edge-role hypotheses force the full principle-constraint bundle on $a$ (down identity, sign relation, positive electroweak of magnitude $A$, and the sum target together imply the principle constraints). Then feed that bundle, with the same down-role hypothesis, into unrestricted forcing from the down role, which concludes $a$ equals the canonical $B_{\mathrm{pow}}$ assignment. No case split or pool enumeration appears.
why it matters
Closes the unrestricted (non-enumerative) half of O1 yardstick forcing for $B_{\mathrm{pow}}$: edge-role algebra alone pins the assignment to the canonical tuple. Downstream, the passive-plus-active-role forcing theorem and the passive/down-role forcing theorem both call this result, packaging the same uniqueness under alternate role presentations (lepton fixed by passive edge count, or passive and down together without an explicit sign hypothesis).
In the broader Recognition chain this protects the mass-ladder yardstick: sector $B_{\mathrm{pow}}$ exponents feed the $\varphi$-ladder mass formula (yardstick $\cdot\varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$). Forcing uniqueness here means the combinatorial choice set really is a singleton, matching the module claim that valid $B_{\mathrm{pow}}$ assignments collapse under structural constraints. It sits on the verification side of the forcing chain rather than on T5--T8 themselves, but it is what makes the yardstick side of those constants checkable without a residual discrete search.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.