yardstick_unrestricted_forcing_from_cube_roles
plain-language theorem explainer
Once cube-role couplings fix the lepton B_pow entry and the up, down, and depth-gap r0 roles, both yardstick layers collapse to their unique canonical assignments. Cite this for O1 yardstick uniqueness without finite enumeration. The proof is a one-line wrapper into a stronger joint forcing lemma, projecting the r0 principle constraints to the needed sum component.
Claim. Let $b$ be a $B_{\mathrm{pow}}$ sector assignment (lepton, up, down, electroweak integers) and $r$ an $r_0$ sector assignment of the same shape. If $b_{\ell}=-(2E_{\mathrm{passive}})$, $b$ meets the $B_{\mathrm{pow}}$ principle constraints, $r_{\mathrm{up}}=2W+A$, $r_{\mathrm{down}}=E_{\mathrm{total}}-W$, $r_{\ell}-r_{\mathrm{ew}}=W-10$, and $r$ meets the $r_0$ principle constraints, then $b$ equals the canonical $B_{\mathrm{pow}}$ assignment and $r$ equals the canonical $r_0$ assignment.
background
The 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 the four sectors (lepton, up, down, electroweak), then filtered by structural constraints. Under those filters the valid choice sets collapse to singletons.
A $B_{\mathrm{pow}}$ assignment and an $r_0$ assignment are each four-tuples of integers, one per sector. Principle constraints package the structural sums and sign/positivity filters used in the yardstick discussion; the canonical assignments are the unique survivors of that filter family. Constants such as $A$ (active edge count per tick, equal to $1$ in the gap derivation) and the passive/total edge counts enter the role equalities as fixed integers.
This theorem is the non-enumerative route: it assumes the cube-role couplings (lepton $B_{\mathrm{pow}}$ fixed to the passive double, and $r_0$ up/down/depth-gap fixed to the stated linear forms in $W$, $A$, and $E_{\mathrm{total}}$) and concludes both layers are forced, without walking the permutation list.
proof idea
One-line term wrapper. It applies the stronger joint lemma yardstick_unrestricted_forcing_from_cube_roles_and_r0_sum, forwarding $b$, $r$, the lepton $B_{\mathrm{pow}}$ equality, the $B_{\mathrm{pow}}$ principle constraints, and the three $r_0$ role equalities unchanged. From the $r_0$ principle-constraint bundle it projects the nested conjunct hrP.2.2.2 (the structural sum component the stronger lemma expects) and stops. No local algebra or case split appears here.
why it matters
In Recognition Science the mass formula is yardstick times a $\varphi$-ladder factor $\varphi^{(\mathrm{rung}-8+\mathrm{gap}(Z))}$. The yardstick itself is fixed by the sector $B_{\mathrm{pow}}$ and $r_0$ layers; uniqueness of those layers is therefore a prerequisite for a unique mass spectrum from the forcing chain.
The module's enumerative path already collapses both choice sets to singletons. This declaration packages the same conclusion as unrestricted forcing from cube-role couplings, so the uniqueness claim does not depend on finite search. The doc-comment states the point directly: once the cube-role couplings are fixed, both yardstick layers are forced to their canonical assignments without finite enumeration.
No downstream consumers are recorded yet; the result sits at the top of the O1 yardstick-uniqueness stack, ready for any theorem that needs canonical $B_{\mathrm{pow}}$ and $r_0$ as input. It does not itself touch T5--T8, but it stabilizes the yardstick side of the mass ladder that those landmarks feed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.