bpow_two_branch_under_down_role
plain-language theorem explainer
Under down-role form, up/EW sign duality, active-unit EW magnitude, and the structural four-sector sum, any integer B_pow assignment collapses to exactly two survivors: the canonical branch or its orientation mirror. Yardstick uniqueness and O1 choice-set arguments cite this residual dichotomy before orientation is fixed. The proof forces the lepton exponent, cases on EW = ±A with A = 1, and matches each case by substitution.
Claim. Let $a$ assign integer $B_{\mathrm{pow}}$ exponents to the lepton, up, down, and electroweak sectors. If $a_{\mathrm{down}} = 2E_{\mathrm{total}}-1$, $a_{\mathrm{up}} = -a_{\mathrm{ew}}$, $|a_{\mathrm{ew}}| = A$ (the active edge count), and $a_{\mathrm{lepton}}+a_{\mathrm{up}}+a_{\mathrm{down}}+a_{\mathrm{ew}}$ equals the structural sum target, then $a$ is either the canonical $B_{\mathrm{pow}}$ assignment or its orientation-mirrored counterpart.
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 constraints until the valid choice set collapses.
A $B_{\mathrm{pow}}$ assignment is simply a 4-tuple of integers, one per sector. The active edge count $A$ is fixed at $1$ in the gap derivation ($\eta_B\cdot\Theta_{\mathrm{crit}}=\varphi^A=\varphi$). The structural sum target is the same numerical constraint used by the yardstick principle (sibling facts record that it equals one and matches the principle form).
The hypotheses encode the down-role formula $2E_{\mathrm{total}}-1$, sign duality between up and electroweak exponents, unit EW magnitude, and the four-way sum. Without an orientation choice those constraints leave a genuine two-element residue: canonical versus mirrored.
proof idea
First apply the auxiliary forcing lemma that, given down-role, sign duality, and the sum, pins the lepton exponent to $-(2E_{\mathrm{passive}})$. Record $A=1$ by computation. Since $|a_{\mathrm{ew}}|=A=1$, case-split on $a_{\mathrm{ew}}=\pm 1$.
In the positive case, sign duality forces $a_{\mathrm{up}}=-A$; destructure the assignment, substitute all four components, and obtain the canonical branch. In the negative case the same steps yield $a_{\mathrm{up}}=+A$ and the mirrored branch. Both arms close by reflexivity after substitution.
why it matters
This is the residual two-branch statement in the O1 yardstick choice-set program: after down-role, sign duality, unit active magnitude, and the structural sum, only canonical and mirrored $B_{\mathrm{pow}}$ assignments survive. The immediate parent bpow_orientation_selects_canonical_from_two_branch adds a positive-EW orientation hypothesis and collapses the disjunction to the canonical branch alone.
That collapse is what lets the module claim that valid $B_{\mathrm{pow}}$ choice sets become singletons under the yardstick structural filters. In the broader RS mass story the yardstick multiplies the $\varphi$-ladder factor $\varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$; fixing the $B_{\mathrm{pow}}$ sector map is a prerequisite for a unique ladder placement. The result does not itself invoke T5–T8 or the RCL, but it is part of the verification layer that makes those forced constants usable in mass assignments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.