yardstick_assignment_forced_from_cube_partition_principle
plain-language theorem explainer
Once sector role kernels and structural sums are fixed, the four-sector B-power and r0 yardstick assignments are uniquely forced to the canonical formulas. Mass-ladder and O1 verification work cites this as the cube-partition uniqueness arrow. The proof is a one-line term wrapper into the unrestricted role-kernel forcing lemma.
Claim. Let $b$ assign integers $(B_{\ell}, B_u, B_d, B_{\mathrm{ew}})$ and $r$ assign integers $(r_{\ell}, r_u, r_d, r_{\mathrm{ew}})$ to the lepton, up, down, and electroweak sectors. If $B_{\ell}=-(2E_{\mathrm{passive}})$, $B_d=2E_{\mathrm{total}}-1$, $B_{\mathrm{ew}}>0$, $|B_{\mathrm{ew}}|=A$, the $B$-sum equals the structural $B$-target, $r_u=2W+A$, $r_d=E_{\mathrm{total}}-W$, $r_{\ell}-r_{\mathrm{ew}}=W-10$, and the $r$-sum equals the structural $r_0$-target, then $b$ and $r$ equal the canonical yardstick assignments.
background
This module treats O1 yardstick uniqueness as a finite combinatorial search: four candidate $B_{\mathrm{pow}}$ values and four candidate $r_0$ values are assigned to the lepton, up, down, and electroweak sectors, then filtered by structural constraints. Valid choice sets collapse to singletons under those filters.
A $B$-power assignment is a 4-tuple of integers, one per sector; an $r_0$ assignment is the analogous depth tuple. The cube-partition package fixes role kernels (passive lepton and down roles for $B$, up/down roles and a lepton–electroweak depth gap for $r_0$) together with additive sum targets that encode vertex/edge exhaustion.
Upstream constants enter as fixed integers: active edge count $A$ (GapDerivation), passive and total edge budgets, and the window parameter $W$. The canonical assignments are the unique survivors of the filtered enumeration; this theorem states the forcing direction from the principle package to those survivors.
proof idea
One-line term proof: apply yardstick_unrestricted_forcing_from_role_kernels_and_sums to the given $B$-power and $r_0$ assignments, forwarding every role-kernel and sum hypothesis unchanged. No extra case split or rewriting occurs at this layer; uniqueness is inherited wholesale from that unrestricted forcing lemma.
why it matters
This is the forcing half of the O1' uniqueness surface. Downstream, yardstick_assignment_iff_cube_partition_principle packages it with the converse into an equivalence: canonical yardstick assignments iff the cube-partition role-kernel plus structural-sum package. It also feeds assignment_valid in the Yardstick Assignment Principle module, which records that the live assignment meets sign duality, complement, and vertex/edge exhaustion.
In the broader Recognition ladder, yardstick uniqueness pins the sector exponents that enter the mass formula (yardstick times $\varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$). Closing O1 as a singleton choice set removes combinatorial freedom before calibration and alpha-band checks. The result is fully proved (no sorry); it does not itself derive the numerical constants $A$, $W$, or the edge budgets, which remain upstream inputs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.