bpow_unrestricted_forcing_from_passive_coupling
plain-language theorem explainer
Once the lepton-sector power is fixed at the passive-edge coupling $-2E_p$, the $B_{\mathrm{pow}}$ principle constraints force any four-sector integer assignment to the canonical one. Yardstick and mass-ladder verifiers cite this to replace finite-pool enumeration by unrestricted algebraic forcing. The proof is integer arithmetic: the lepton-down sum target, complementarity, and sign pattern pin down, electroweak, and up from that single input.
Claim. Let $a=(a_\ell,a_u,a_d,a_{\mathrm{ew}})$ be an integer power assignment to the lepton, up, down, and electroweak sectors. If $a_\ell=-2E_{\mathrm{passive}}$ and $a$ obeys the $B_{\mathrm{pow}}$ principle constraints (sign pattern, complementarity of absolute values, $a_u<0$, $a_{\mathrm{ew}}>0$, and the lepton-down sum target), then $a$ equals the canonical $B_{\mathrm{pow}}$ assignment $(-22,-1,23,1)$.
background
This module treats the O1 yardstick discussion as a finite combinatorial search: four candidate $B_{\mathrm{pow}}$ values and four $r_0$ values, all sector-to-value permutations, filtered by structural constraints. Valid choice sets collapse to singletons for both layers.
A $B_{\mathrm{pow}}$ assignment is a 4-tuple of integers (lepton, up, down, electroweak). The principle constraints package the sign pattern, a complementarity relation on absolute values, negativity of the up entry, positivity of the electroweak entry, and a lepton-down sum equal to a fixed target (proved equal to $1$). The passive-edge coupling input is $a_\ell=-2E_{\mathrm{passive}}$, which evaluates to $-22$.
The unrestricted theorems drop membership in the finite value pool: principle constraints plus one role coupling already force the canonical assignment. Downstream joint yardstick forcing uses the same lepton-role hypothesis on the $B_{\mathrm{pow}}$ layer.
proof idea
Destructure the principle-constraint bundle into sign, complementarity, up-negativity, electroweak positivity, and sum. From the sum conjunct and the sign pattern, obtain $a_\ell+a_d$ equal to the sum target, then rewrite that target as $1$.
Substitute the lepton hypothesis and evaluate $-2E_{\mathrm{passive}}=-22$ by native decision. Linear arithmetic then gives $a_d=23$. Complementarity with the absolute values of lepton and down forces $|a_{\mathrm{ew}}|=1$; positivity upgrades this to $a_{\mathrm{ew}}=1$. The sign pattern then forces $a_u=-1$.
Destructure the assignment structure, substitute the four forced components, and close by reflexivity against the canonical tuple.
why it matters
This is the first unrestricted $B_{\mathrm{pow}}$ forcing lemma in the choice-set module: no finite-pool filter is required once the lepton sector sits at passive-edge coupling $-2E_p$. It feeds the weaker-input sibling that starts from the down-sector role $2E_{\mathrm{total}}-1$, and the joint theorem that forces both yardstick layers from cube-role couplings plus the $r_0$ structural sum.
In the Recognition mass ladder, sector powers enter the yardstick prefactor of the $\varphi$-rung formula. Collapsing the $B_{\mathrm{pow}}$ choice set to a singleton is O1 progress toward a unique yardstick assignment without enumeration. The result sits in the verification layer rather than the T0-T8 forcing chain, but it hardens the constants that later calibrate masses against the $\varphi$-ladder and the eight-tick octave bookkeeping.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.