r0_unrestricted_forcing_from_affine_roles_and_sum
plain-language theorem explainer
Fixing the cube-hierarchy affine roles for the up and down rungs, the lepton–EW depth gap, and the structural four-sector sum already pins every integer in an r0 assignment to the canonical values (62, 35, −5, 55). Anyone citing unrestricted yardstick uniqueness without finite-pool enumeration needs this lemma. The proof evaluates the affine formulas by native decision, recovers the remaining two rungs by linear arithmetic, and closes by substitution.
Claim. Let $a$ be an integer 4-tuple $(r_\ell, r_u, r_d, r_{\mathrm{EW}})$ of sector rungs. If $r_u = 2W+A$, $r_d = E_{\mathrm{total}}-W$, $r_\ell-r_{\mathrm{EW}}=W-10$, and $r_\ell+r_u+r_d+r_{\mathrm{EW}}$ equals the structural $r_0$ sum target, then $a$ equals the canonical assignment $(62,35,-5,55)$.
background
The module treats O1 yardstick assignment as a finite combinatorial search over sector-to-value maps for both $B_{\mathrm{pow}}$ and $r_0$, then filters by the structural constraints of the Yardstick discussion. Valid choice sets collapse to singletons. An $r_0$ assignment is simply four integers, one per sector: lepton, up, down, and electroweak.
The affine role formulas come from the cube hierarchy: up is $2W+A$, down is $E_{\mathrm{total}}-W$, and the lepton–EW depth gap is $W-10$. The structural sum target is the constant $147$ (proved equal to r0SumTarget elsewhere in the module). Canonical $r_0$ is the unique 4-tuple that survives those constraints.
This lemma is the unrestricted (no finite-pool membership) forcing step: the roles plus gap plus sum alone determine the assignment, without enumerating permutations.
proof idea
Rewrite the sum hypothesis via r0_sum_target_eq_147 to get total $147$. Evaluate the three affine formulas by native_decide: up becomes $35$, down becomes $-5$, and the depth gap becomes $7$. From the sum and the two fixed rungs, nlinarith yields lepton$+$EW $=117$; combining with the gap then forces lepton $=62$ and EW $=55$. Destructure the assignment structure, substitute the four equalities, and close by rfl.
why it matters
This is the core unrestricted uniqueness engine for the $r_0$ layer of the yardstick. Downstream it feeds r0_principle_constraints_forced_from_affine_roles_and_sum (principle constraints become derived, no independent order axioms), the iff form equating principle constraints to the sum alone under affine roles and gap, and the alternate forcing routes that swap the gap for an EW affine role or package full principle constraints. Joint yardstick theorems then lift the same pattern to both $B_{\mathrm{pow}}$ and $r_0$ layers without finite enumeration.
In the broader RS picture this locks the integer rungs that enter the mass formula (yardstick $\cdot\varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$ on the $\varphi$-ladder). It is verification infrastructure for O1, not a new forcing-chain step (T5–T8), but it closes the combinatorial ambiguity that would otherwise leave sector rungs free.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.