bpow_principle_iff_active_unit_under_passive_down_roles
plain-language theorem explainer
Under fixed lepton and down roles (passive and total-edge formulas) plus the structural four-sector sum and positive electroweak entry, the B_pow principle constraints hold exactly when the electroweak absolute value equals the active-edge count A. Yardstick/O1 enumerators cite this to collapse sector assignments. Proof derives the forced up-sign, then applies the down-role equivalence.
Claim. Let $a$ assign integers $(B_\ell, B_u, B_d, B_{ew})$ to the lepton, up, down, and electroweak sectors. Suppose $B_\ell = -2 E_{\mathrm{passive}}$, $B_d = 2 E_{\mathrm{total}} - 1$, $B_\ell + B_u + B_d + B_{ew}$ equals the B_pow sum target, and $B_{ew} > 0$. Then the B_pow principle constraints hold on $a$ if and only if $|B_{ew}| = A$, where $A$ is the active-edge count per tick.
background
The 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 and principle constraints. Valid choice sets are meant to collapse to singletons.
A BPowAssignment is just an integer 4-tuple for those sectors. Anchor constants fix the edge bookkeeping: passive edges $E_{\mathrm{passive}} = 11$ (from $12-1$), active edges per tick $A = 1$, and $E_{\mathrm{total}}$ the total edge count entering the down-role formula. The sum target is the fixed integer that principle-level yardstick bookkeeping demands of the four exponents.
This statement is the passive/down specialization of the more general down-role equivalence: lepton and down are pinned to the passive and total-edge formulas, the structural sum is assumed, and the up-sector sign is not hypothesized but derived.
proof idea
Two-step term proof. First apply bpow_sign_forced_from_lepton_down_sum to the lepton, down, and sum hypotheses to obtain $a.{\mathrm{up}} = -a.{\mathrm{ew}}$. Then feed that forced sign, together with the down-role, sum, and positivity hypotheses, into bpow_principle_iff_active_unit_under_down_role, which already equates principle constraints with $|a.{\mathrm{ew}}| = A$. No extra algebra is done here.
why it matters
In the Recognition yardstick story, sector $B_{\mathrm{pow}}$ exponents must match anchor edge counts so the mass ladder (yardstick $\cdot \varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$) stays consistent. This lemma closes the passive/down specialization of that filter: once lepton and down are locked to $E_{\mathrm{passive}}$ and $E_{\mathrm{total}}$, principle constraints reduce to the electroweak sector carrying absolute value $A = 1$.
It is consumed by bpow_bool_constraints_iff_active_unit_under_passive_down_roles, the Boolean-filter form used in the choice-set enumeration. That enumeration is the O1 progress claim of the module: under structural constraints the valid $B_{\mathrm{pow}}$ assignments collapse to a singleton. The result is local verification scaffolding, not a forcing-chain (T0–T8) step, but it hardens the unique yardstick assignment that later mass and $\alpha$ checks rely on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.