r0_unrestricted_forcing_from_affine_roles_and_ew_role
plain-language theorem explainer
Under affine role formulas for the up, down, and electroweak sector integers of an r0 assignment, plus the structural four-sector sum, the assignment equals the canonical r0. Mass-ladder and yardstick verifiers cite this as an unrestricted uniqueness route (no finite-pool membership). The proof forces the lepton–electroweak depth gap from the electroweak role via an iff, then applies the affine-roles-plus-depth-gap forcing theorem.
Claim. Let $a=(r_0^{\ell},r_0^{u},r_0^{d},r_0^{\mathrm{ew}})$ be an integer assignment to the lepton, up, down, and electroweak sectors. If $r_0^{u}=2W+A$, $r_0^{d}=E_{\mathrm{total}}-W$, $r_0^{\mathrm{ew}}=3W+4$, and $r_0^{\ell}+r_0^{u}+r_0^{d}+r_0^{\mathrm{ew}}$ equals the r0 sum target, then $a$ equals the canonical r0 assignment.
background
This module treats the O1 yardstick discussion as a finite combinatorial search: candidate integer values for sector powers $B_{\mathrm{pow}}$ and rungs $r_0$ are assigned to lepton, up, down, and electroweak sectors, then filtered by structural constraints. Valid choice sets collapse to singletons for both $B_{\mathrm{pow}}$ and $r_0$.
An r0 assignment is a four-tuple of integers, one per sector. The unrestricted forcing path does not require membership in a pre-enumerated finite pool; it works from affine role identities and a sum target alone. The constants $W$, $A$, and $E_{\mathrm{total}}$ enter as fixed integers from the gap and edge-count layer ($A$ is the active edge count per tick, equal to 1 in the gap derivation).
The companion route assumes affine up/down roles together with an explicit depth-gap identity $r_0^{\ell}-r_0^{\mathrm{ew}}=W-10$. The present statement replaces that gap hypothesis by an affine electroweak role $r_0^{\mathrm{ew}}=3W+4$, which is equivalent to the gap once up/down roles and the sum are fixed.
proof idea
Two-step term proof. First apply the reverse direction of the iff lemma that, under affine up/down roles and the structural sum, the electroweak affine role is equivalent to the depth-gap identity $a.{\mathrm{lepton}}-a.{\mathrm{ew}}=W-10$; instantiate it on the given electroweak-role hypothesis to obtain the gap. Then feed affine up/down roles, that derived gap, and the sum into the already-proved unrestricted forcing theorem (affine roles plus depth gap plus sum imply equality with the canonical r0).
why it matters
In Recognition Science the mass formula is yardstick times $\varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$ on the phi-ladder, so the integer r0 sector assignment must be unique once structural roles are fixed. This theorem supplies an alternate unrestricted uniqueness route: electroweak affine role in place of an a-priori depth gap, still concluding canonical r0.
It sits in the O1 yardstick choice-set program, whose module goal is that filtered assignment sets collapse to singletons. Downstream use count is currently zero; the declaration is a leaf alternate entry point parallel to the depth-gap form, useful when a derivation naturally produces the electroweak role $3W+4$ rather than the gap $W-10$. No forcing-chain step T0–T8 is discharged here; the result is verification infrastructure for the yardstick layer above those landmarks.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.