bpow_principle_constraints_forced_from_passive_active_roles
plain-language theorem explainer
Under a passive-edge lepton role, opposite up/EW signs, positive EW of magnitude A, and the four-sector sum target, any integer B_pow assignment satisfies the full principle constraint package. Yardstick-enumeration and O1 uniqueness arguments cite this when the lepton role is the natural input rather than the down role. The proof converts the lepton hypothesis into the down-role equation, then reuses the edge-role forcing lemma.
Claim. Let $a$ assign integers $B_{\mathrm{pow}}$ to the lepton, up, down, and electroweak sectors. If $a_{\ell}=-(2E_{\mathrm{passive}})$, $a_{u}=-a_{\mathrm{ew}}$, $a_{\mathrm{ew}}>0$, $|a_{\mathrm{ew}}|=A$, and $a_{\ell}+a_{u}+a_{d}+a_{\mathrm{ew}}$ equals the fixed sum target, then $a$ satisfies the principle $B_{\mathrm{pow}}$ constraints.
background
This 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 and filtered by structural and principle constraints until only a singleton survives.
A BPowAssignment is simply four integers $(a_\ell,a_u,a_d,a_{\mathrm{ew}})$. The constant $A$ is the active-edge count per tick ($A=1$ in the gap derivation). Passive and total edge counts $E_{\mathrm{passive}}$, $E_{\mathrm{total}}$ fix the lepton and down roles on the recognition ledger. The sum target is the unique integer that the four sector powers must add to under the yardstick principle.
An earlier sibling forces the principle package from an explicit down-role hypothesis $a_d=2E_{\mathrm{total}}-1$ together with the sign, positivity, magnitude, and sum conditions. The present theorem is the same derivation with the passive-edge lepton role as the primary input.
proof idea
Term-mode, two steps. First apply the equivalence bpow_lepton_role_iff_down_role_under_sign_sum: given the opposite-sign relation $a_u=-a_{\mathrm{ew}}$ and the four-sector sum, the lepton role $a_\ell=-(2E_{\mathrm{passive}})$ is equivalent to the down role $a_d=2E_{\mathrm{total}}-1$. Project the forward direction to obtain the down equation. Then feed that equation, together with the unchanged sign, positivity, magnitude, and sum hypotheses, into bpow_principle_constraints_forced_from_edge_roles, which already packages the full principle constraint set.
why it matters
In the O1 yardstick discussion the valid $B_{\mathrm{pow}}$ choice set collapses to a singleton once principle constraints are imposed. This theorem supplies the forcing step when the natural physical input is the passive-edge lepton role rather than an a-priori down assignment, matching the ledger's passive/active edge split ($A=1$ active edges per tick).
It is consumed immediately by the Boolean-filter sibling bpow_bool_constraints_forced_from_passive_active_roles, which turns the same hypotheses into a decidable predicate for the finite enumeration. That filter is what makes the combinatorial search certify uniqueness of the yardstick powers used in the mass formula (yardstick $\cdot\varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$ on the $\varphi$-ladder). No new physics is introduced; the result is a role-input variant that closes the passive-edge entry point into the already-proved edge-role forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.