yardstick_unrestricted_forcing_from_cube_roles_and_r0_sum
plain-language theorem explainer
Once cube-role couplings fix the lepton passive slot on B_pow and the affine up/down/depth-gap roles on r0, together with the r0 structural sum, both yardstick layers equal their unique canonical assignments. Mass-ladder and O1 verification work cites this to replace finite permutation search by direct forcing. The proof is a two-conjunct term pairing the B_pow passive-coupling forcer with the r0 affine-role-and-sum forcer.
Claim. Let $b$ assign integers $(B_{\mathrm{pow}})$ to the lepton, up, down, and electroweak sectors, and let $r$ assign integers $(r_0)$ to the same four sectors. Suppose $b_{\mathrm{lepton}}=-(2E_{\mathrm{passive}})$, $b$ satisfies the B_pow principle constraints, $r_{\mathrm{up}}=2W+A$, $r_{\mathrm{down}}=E_{\mathrm{total}}-W$, $r_{\mathrm{lepton}}-r_{\mathrm{ew}}=W-10$, and $r_{\mathrm{lepton}}+r_{\mathrm{up}}+r_{\mathrm{down}}+r_{\mathrm{ew}}$ equals the $r_0$ sum target. Then $b$ equals the canonical $B_{\mathrm{pow}}$ assignment and $r$ equals the canonical $r_0$ assignment.
background
The module treats O1 yardstick assignment as a finite combinatorial search: four candidate $B_{\mathrm{pow}}$ values and four candidate $r_0$ values are permuted across the lepton, up, down, and electroweak sectors, then filtered by structural constraints from the Yardstick discussion. Under those filters both choice sets collapse to singletons.
A $B_{\mathrm{pow}}$ assignment is a four-tuple of integers (lepton, up, down, ew); an $r_0$ assignment is the same shape for the second yardstick layer. The passive-coupling hypothesis pins the lepton $B_{\mathrm{pow}}$ slot to $-(2E_{\mathrm{passive}})$. Principle constraints on $b$ encode the remaining structural filters used in the yardstick principle. On the $r_0$ side, affine cube roles fix up as $2W+A$ and down as $E_{\mathrm{total}}-W$, a depth gap relates lepton and ew by $W-10$, and the four components sum to the fixed $r_0$ target (known to equal one in the sibling sum lemmas).
Upstream constants such as the active edge count $A$ (GapDerivation) and species thresholds for up/down enter the role formulas; the forcing is meant to recover the same canonical layers that the enumeration path isolates.
proof idea
Term-mode pairing of two already-proved unrestricted forcers. The left conjunct applies bpow_unrestricted_forcing_from_passive_coupling to $b$ with the lepton passive-coupling equality and the principle-constraint hypothesis, yielding $b=$ canonical $B_{\mathrm{pow}}$. The right conjunct applies r0_unrestricted_forcing_from_affine_roles_and_sum to $r$ with the up-role, down-role, depth-gap, and structural-sum hypotheses, yielding $r=$ canonical $r_0$. No further case split or enumeration appears at this layer.
why it matters
Closes the joint unrestricted path for both yardstick layers once cube-role couplings are fixed, without relying on finite permutation enumeration. The immediate parent is yardstick_unrestricted_forcing_from_cube_roles, which packages the same joint claim (doc: "once the cube-role couplings are fixed, both yardstick layers are forced to their canonical assignments without finite enumeration"). This variant is the sum-only $r_0$ form: order/filter conjuncts are derived from affine roles plus the depth gap rather than assumed outright.
In the broader Recognition ladder, canonical $B_{\mathrm{pow}}$ and $r_0$ feed the mass formula (yardstick $\cdot \varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$) and the O1 verification that sector assignments are unique. The result sits in the Verification domain as a bridge from structural cube roles (W, A, $E_{\mathrm{passive}}$, $E_{\mathrm{total}}$) to the forced anchors used downstream of the forcing chain (T5–T8, phi-ladder).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.