yardstick_unrestricted_forcing_from_role_kernels_and_sums
plain-language theorem explainer
Once cube-role kernels and structural sums are fixed for both yardstick layers, the sector-to-value maps for B_pow and r0 are uniquely the canonical assignments. Mass-ladder and O1 verification work cites this to replace finite choice-set enumeration by algebraic forcing. The proof is a paired term that applies the B_pow passive/down-role forcer and the r0 affine-role 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_{\ell}=-(2E_{\mathrm{passive}})$, $b_{d}=2E_{\mathrm{total}}-1$, $b_{\mathrm{ew}}>0$, $|b_{\mathrm{ew}}|=A$, and $\sum b=B_{\mathrm{pow}}^{\mathrm{target}}$; and suppose $r_{u}=2W+A$, $r_{d}=E_{\mathrm{total}}-W$, $r_{\ell}-r_{\mathrm{ew}}=W-10$, and $\sum r=r_0^{\mathrm{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, all sector permutations, filtered by structural constraints from the Yardstick discussion. Valid choice sets collapse to singletons under those filters.
A $B_{\mathrm{pow}}$ assignment is a four-tuple of integers (lepton, up, down, electroweak). An $r_0$ assignment is the same shape for the second yardstick layer. Role-kernel hypotheses pin selected components to closed-form expressions in the framework constants $E_{\mathrm{passive}}$, $E_{\mathrm{total}}$, $A$, and $W$; the remaining freedom is killed by a single structural sum target on each layer ($B_{\mathrm{pow}}^{\mathrm{target}}$, $r_0^{\mathrm{target}}$).
This statement is the unrestricted (non-enumerative) route: it does not assume the full boolean filter bundles, only the role kernels plus sums. The electroweak magnitude condition $|b_{\mathrm{ew}}|=A$ is the active-unit constraint that, under passive/down roles, is equivalent to the structural $B_{\mathrm{pow}}$ filter.
proof idea
Term-mode pairing of two already-proved layer forcers. The left conjunct is bpow_unrestricted_forcing_from_passive_down_roles applied to $b$ with the five $B_{\mathrm{pow}}$ hypotheses (passive lepton, down role, electroweak positivity and magnitude $A$, and the $B_{\mathrm{pow}}$ sum). The right conjunct is r0_unrestricted_forcing_from_affine_roles_and_sum applied to $r$ with the four $r_0$ hypotheses (up and down affine roles, lepton–electroweak depth gap $W-10$, and the $r_0$ sum). No extra tactics; the conjunction is the theorem statement.
why it matters
Feeds directly into yardstick_assignment_forced_from_cube_partition_principle, whose doc-comment states the cube-partition first-principles claim: once role kernels and structural sums are fixed, sector yardstick assignments are uniquely forced to the canonical formulas. That parent is the bridge from combinatorial O1 enumeration to a principle-level uniqueness theorem.
In the Recognition mass story the yardstick sits in front of the $\varphi$-ladder formula (yardstick $\times \varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$). Forcing both layers without enumeration removes a residual discrete ambiguity in how sectors couple to the ladder. The constants $A$ and $W$ entering the role kernels sit in the same arithmetic spine as the gap derivation and cost-projector structure used elsewhere in the forcing chain.
Closes the unrestricted half of the O1 progress narrative in this module: filters that previously looked like search constraints become consequences of role kernels plus sums.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.