bpow_sign_forced_from_lepton_down_sum
plain-language theorem explainer
Fixing the lepton sector to the passive-edge value and the down sector to the total-edge odd value, the structural four-sector sum forces the up and electroweak exponents to be exact negatives. Yardstick-assignment and O1 forcing arguments cite this to drop an explicit sign hypothesis. The proof evaluates the two fixed roles to integers and closes by linear arithmetic on the sum identity.
Claim. Let $a$ assign integers $(a_\ell, a_u, a_d, a_{\mathrm{ew}})$ to the lepton, up, down, and electroweak sectors. If $a_\ell = -(2 E_{\mathrm{passive}})$, $a_d = 2 E_{\mathrm{total}} - 1$, and $a_\ell + a_u + a_d + a_{\mathrm{ew}}$ equals the structural $B_{\mathrm{pow}}$ sum target (equal to $1$), then $a_u = -a_{\mathrm{ew}}$.
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 constraints until only a singleton remains.
A BPowAssignment is simply that four-tuple of integer exponents. The passive-edge lepton role sets the lepton exponent to $-(2 E_{\mathrm{passive}})$; numerically this is $-22$. The down role sets the down exponent to $2 E_{\mathrm{total}} - 1$, numerically $23$. The structural sum target for the four exponents is the constant bpowSumTarget, proved equal to $1$.
Active-edge sign duality means the remaining two exponents (up and electroweak) sum to zero, i.e. are exact negatives. Downstream results use that duality to select the canonical orientation without stating a separate sign hypothesis.
proof idea
Rewrite the sum hypothesis via bpow_sum_target_eq_one to get $a_\ell + a_u + a_d + a_{\mathrm{ew}} = 1$. Evaluate the two role hypotheses by native_decide: $a_\ell = -22$ and $a_d = 23$. Linear arithmetic (nlinarith) on those three equalities yields $a_u + a_{\mathrm{ew}} = 0$, hence $a_u = -a_{\mathrm{ew}}$. No external lemmas beyond the sum-target identity are required.
why it matters
This is the algebraic hinge that lets passive/down role data imply active-edge sign duality. Four parents consume it directly: bpow_orientation_selects_canonical_from_passive_down_roles (branch selection without an explicit sign assumption), bpow_principle_iff_active_unit_under_passive_down_roles (principle constraints equivalent to unit EW magnitude with sign derived internally), bpow_unrestricted_forcing_from_passive_down_roles (unrestricted canonical forcing), and yardstick_filter_family_forced_from_cube_partition_principle (cube-partition packaging of the full $B_{\mathrm{pow}}$ and $r_0$ admissibility filter).
In the Recognition mass story the $B_{\mathrm{pow}}$ exponents sit on the phi-ladder yardstick; collapsing their sign freedom is part of forcing a unique admissible assignment rather than enumerating a residual choice set. The result is pure integer arithmetic on role constants, so it closes a combinatorial gap without touching the deeper T5–T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.