bpow_orientation_selects_canonical_from_passive_down_roles
plain-language theorem explainer
Under passive lepton and down-sector role fixings, the structural B_pow sum, unit electroweak magnitude, and positive EW orientation, any four-sector integer assignment equals the canonical B_pow. Anyone closing O1 yardstick choice-set uniqueness would cite this. The proof first forces sign-duality from the sum, then applies the two-branch orientation selector.
Claim. Let $a$ assign integers to the lepton, up, down, and electroweak sectors. If $a_{\mathrm{lepton}} = -2 E_{\mathrm{passive}}$, $a_{\mathrm{down}} = 2 E_{\mathrm{total}} - 1$, $|a_{\mathrm{ew}}| = A$ (active-edge count), the four values 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 structural constraints until the valid choice set collapses to a singleton.
A BPowAssignment is simply a 4-tuple of integers, one per sector. The canonical assignment is the distinguished survivor of that filter. The constant $A$ is the active-edge count per tick ($A = 1$). The structural sum target is the fixed total that every admissible assignment must hit.
The passive and down role formulas pin two of the four coordinates. The remaining freedom is orientation (sign pattern) and the electroweak magnitude. Upstream, the two-branch selector already shows that down-role plus explicit sign-duality plus unit EW magnitude plus positive EW orientation force canonicity; the present result removes the need to assume sign-duality by hand.
proof idea
Term-mode, two steps. First apply bpow_sign_forced_from_lepton_down_sum: the passive-lepton and down-role fixings together with the structural sum force $a_{\mathrm{up}} = -a_{\mathrm{ew}}$ (sign-duality). Then feed that derived equality, along with the down-role, unit EW magnitude, sum, and positive-EW hypotheses, into bpow_orientation_selects_canonical_from_two_branch, which returns equality with the canonical assignment.
why it matters
Closes a convenience gap in the O1 yardstick choice-set argument: once lepton is fixed to the passive role and down to its sector formula, sign-duality is no longer an independent hypothesis. The module's stated goal is that valid $B_{\mathrm{pow}}$ (and $r_0$) choice sets collapse to singletons under structural constraints; this theorem is one of the orientation-selection lemmas that make that collapse hold without redundant assumptions.
It sits downstream of the two-branch selector and the sign-forcing lemma, and upstream of any uniqueness statement that wants the weakest possible hypothesis package. No further used-by edges are recorded yet. In the broader Recognition chain it supports the mass-yardstick side of the phi-ladder (masses as yardstick times $\varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$), by locking which sector carries which $B_{\mathrm{pow}}$ exponent.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.