bpow_orientation_selects_canonical_from_two_branch
plain-language theorem explainer
Under the two-branch structural constraints on a four-sector B_pow assignment, positive electroweak orientation forces the assignment to equal the canonical labeling. Yardstick and mass-ladder verification cite this to pin a unique admissible B_pow choice. The proof cases on the two-branch dichotomy and kills the mirror branch by a native check that its electroweak component is non-positive.
Claim. Let $a$ assign integers $B_{\mathrm{pow}}$ 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$ (active edge count), the four components sum to the structural $B_{\mathrm{pow}}$ target, and $a_{\mathrm{ew}}>0$, 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 the structural constraints used in the yardstick principle. Valid choice sets are meant to collapse to singletons.
A $B_{\mathrm{pow}}$ assignment is simply a 4-tuple of integers, one per sector. The canonical and mirrored assignments are the two surviving candidates once the down-role, magnitude, sign-duality, and sum constraints are imposed. The sum target is the structural total fixed by the yardstick principle (equal to one in the native normalization). Here $A$ is the active edge count per tick ($A=1$ in the gap derivation), and $E_{\mathrm{total}}$ is the total energy/exponent anchor from the mass-anchor layer.
The immediate upstream fact is the two-branch lemma: under down-role, up/EW sign duality, EW magnitude $A$, and the structural sum, every such assignment is either the canonical tuple or its mirror.
proof idea
Apply the two-branch lemma under the down-role, sign-duality, magnitude, and sum hypotheses. That yields a disjunction: the assignment equals the canonical $B_{\mathrm{pow}}$ tuple, or it equals the mirrored tuple.
The first disjunct is the goal. On the second, rewrite the positivity hypothesis along the mirror equality, then contradict it by a native decision that the mirrored electroweak component is not strictly positive. Hence only the canonical branch survives.
why it matters
In the Recognition mass formula, sector masses sit on a $\varphi$-ladder scaled by a yardstick; $B_{\mathrm{pow}}$ is part of that sector labeling. The module's O1 program is to show the admissible assignments collapse to a singleton once structural filters run.
This theorem is the orientation cut: after the two-branch reduction, positivity of the electroweak component selects the canonical labeling and discards the mirror. The immediate parent is the passive/down-roles form, which drops the explicit sign-duality hypothesis because passive and down roles already force it, then reuses this orientation argument.
Together these steps turn the yardstick choice set from an enumerated pool into a unique canonical $B_{\mathrm{pow}}$ assignment, closing one combinatorial degree of freedom in the verification chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.