bpow_unrestricted_forcing_from_passive_active_roles
plain-language theorem explainer
Any integer assignment of B_pow exponents to the lepton, up, down, and electroweak sectors that matches the passive-edge lepton role, the opposite-sign up/EW pair, positive EW magnitude equal to the active-edge count A, and the global sum target must equal the canonical assignment. Yardstick and mass-ladder uniqueness arguments cite this. The proof converts the lepton role into the down-edge role via an iff lemma, then applies the unrestricted edge-role forcing theorem.
Claim. Let $a$ be an integer 4-tuple $(a_\ell, a_u, a_d, a_{\mathrm{ew}})$ of $B_{\mathrm{pow}}$ sector exponents. If $a_\ell = -2 E_{\mathrm{passive}}$, $a_u = -a_{\mathrm{ew}}$, $a_{\mathrm{ew}} > 0$, $|a_{\mathrm{ew}}| = A$ (the active-edge count), and $a_\ell + a_u + a_d + a_{\mathrm{ew}}$ equals the fixed sum target, then $a$ equals the canonical $B_{\mathrm{pow}}$ assignment.
background
This module treats the O1 yardstick discussion as a finite combinatorial search: four candidate $B_{\mathrm{pow}}$ values are assigned to the four sectors (lepton, up, down, electroweak), then filtered by structural and principle constraints until only a singleton remains.
A BPowAssignment is simply an integer 4-tuple of those sector exponents. The sum target is the fixed integer that all admissible assignments must hit (equal to 1 under the principle constraints). The constant $A$ is the active-edge count per tick from the gap derivation ($A = 1$). The quantities $E_{\mathrm{passive}}$ and $E_{\mathrm{total}}$ encode the passive-edge and total-edge role normalizations used to pin lepton and down exponents.
The companion edge-role forcing result already shows that fixing the down exponent to $2E_{\mathrm{total}}-1$, together with the sign, positivity, magnitude, and sum hypotheses, collapses every assignment to the canonical one. The present theorem supplies the passive-edge (lepton) entry point into that same collapse.
proof idea
Term-mode, two steps. First apply the left-to-right direction of the iff lemma relating lepton and down roles under the sign and sum hypotheses: from $a_\ell = -2E_{\mathrm{passive}}$ deduce $a_d = 2E_{\mathrm{total}}-1$. Then feed that down-role equality, together with the unchanged sign, positivity, magnitude, and sum hypotheses, into the unrestricted edge-role forcing theorem, which returns $a$ equal to the canonical assignment.
why it matters
In the Recognition mass formula the yardstick multiplies $\varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$ on the phi-ladder; uniqueness of the $B_{\mathrm{pow}}$ sector exponents is therefore part of locking the absolute mass scale. This theorem closes the passive-edge entry route into that uniqueness: once lepton is fixed by the passive role, the assignment is forced without enumerating the full choice set.
It sits in the O1 progress track of the yardstick assignment module, where structural and principle filters already collapse both $B_{\mathrm{pow}}$ and $r_0$ choice sets to singletons. No downstream consumers are wired yet; the natural parents are the full unrestricted canonical-forcing statements and any later verification that the physical yardstick equals the canonical tuple. Framework landmarks touched: the phi-ladder mass formula and the active-edge count $A$ from the gap derivation (linked to $\eta_B\cdot\Theta_{\mathrm{crit}}=\varphi^A$).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.