bpow_unrestricted_forcing_from_passive_down_roles
plain-language theorem explainer
Given a four-sector integer B_pow assignment, fixing the lepton slot to the passive-role kernel, the down slot to the total-energy kernel, a positive electroweak entry of active-unit magnitude A, and the structural four-sum, forces the assignment to equal the canonical B_pow tuple. Downstream joint yardstick forcing cites this as the B_pow half of unrestricted role-kernel forcing. The proof first recovers the missing up/ew sign duality from the sum, then applies edge-role forcing.
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$, $a_{\mathrm{ew}} > 0$ with $|a_{\mathrm{ew}}| = A$ (active edge count), and $a_\ell + a_u + a_d + a_{\mathrm{ew}}$ equals the structural $B_{\mathrm{pow}}$ sum target, 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 and four candidate $r_0$ values are assigned to sectors by permutation, then filtered by the structural constraints of the Yardstick Assignment Principle. Valid choice sets collapse to singletons for both layers.
A BPowAssignment is simply an integer 4-tuple (lepton, up, down, electroweak). The structural sum target is the fixed total those four entries must meet (equal to one in the principle normalization). The constant $A$ is the active edge count per tick, fixed at $1$ in the gap derivation. Passive and total energy integers $E_{\mathrm{passive}}$, $E_{\mathrm{total}}$ supply the role-kernel formulas for the lepton and down slots.
The companion edge-role forcing result already concludes canonicity once the down kernel, the sign duality $a_u = -a_{\mathrm{ew}}$, the positive electroweak magnitude, and the sum are known. The present theorem removes the need to assume that sign duality up front.
proof idea
Two-step term proof. First apply the in-module lemma that, from the passive lepton kernel, the down kernel, and the structural four-sum alone, forces $a_u = -a_{\mathrm{ew}}$ (sign duality between up and electroweak). Then feed that derived equality, together with the given down kernel, electroweak positivity, magnitude $|a_{\mathrm{ew}}| = A$, and the same sum, into the unrestricted edge-role forcing theorem, which returns $a$ equal to the canonical $B_{\mathrm{pow}}$ assignment.
why it matters
Closes the B_pow half of unrestricted yardstick forcing without an explicit orientation or sign hypothesis: passive/down role kernels plus sum and active-unit magnitude already pin the canonical branch. The sole downstream consumer is the joint theorem that, once cube-role couplings are fixed, both yardstick layers ($B_{\mathrm{pow}}$ and $r_0$) are forced by role-kernel assumptions and structural sums, without finite enumeration and without assuming full filter bundles.
In the broader Recognition picture this is verification scaffolding for the mass-yardstick layer on the phi-ladder (masses as yardstick times $\varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$). It supports the claim that the O1 choice set is not an open combinatorial menu but a forced singleton once passive/down roles and the structural sum are imposed, aligning with the forcing-chain style of T5–T8 uniqueness arguments rather than ad hoc sector bookkeeping.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.