yardstick_assignment_iff_cube_partition_principle
plain-language theorem explainer
Canonical yardstick power and rung-offset assignments on the four mass sectors are exactly the assignments that satisfy the cube-partition role-kernel equalities plus the two structural sum targets. Cite this when stating O1 uniqueness of the mass-ladder yardstick in iff form. Forward direction substitutes the canonical values and decides the arithmetic; reverse applies the forced-assignment lemma from the same package.
Claim. Let $b$ and $r$ be integer assignments of powers and rung offsets to the four sectors (lepton, up, down, electroweak). Then $b$ and $r$ equal the canonical yardstick assignments if and only if $b_{\mathrm{lepton}}=-2E_{\mathrm{passive}}$, $b_{\mathrm{down}}=2E_{\mathrm{total}}-1$, $b_{\mathrm{ew}}>0$ with $|b_{\mathrm{ew}}|=A$, the four $b$-components sum to the power sum target, $r_{\mathrm{up}}=2W+A$, $r_{\mathrm{down}}=E_{\mathrm{total}}-W$, $r_{\mathrm{lepton}}-r_{\mathrm{ew}}=W-10$, and the four $r$-components sum to the rung-offset sum target.
background
This module treats O1 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 the structural constraints of the yardstick discussion. Valid choice sets collapse to singletons for both families.
A power assignment is a 4-tuple of integers $(b_{\mathrm{lepton}},b_{\mathrm{up}},b_{\mathrm{down}},b_{\mathrm{ew}})$; a rung-offset assignment is the analogous 4-tuple for $r$. Anchor constants fix the arithmetic: active edges per tick $A=1$, passive edge count $E_{\mathrm{passive}}=11$, together with $E_{\mathrm{total}}$ and the wallpaper integer $W$. The power sum target and rung-offset sum target are the fixed totals those 4-tuples must hit.
The right-hand side packages the cube-partition role kernel (passive/down roles for powers; up/down/depth-gap roles for offsets) with the two structural sums. The left-hand side is equality to the unique canonical pair produced by that filter.
proof idea
Iff is split by constructor.
Forward: assume $b$ and $r$ are the canonical assignments; substitute both; discharge every conjunct by native_decide (pure integer arithmetic on Anchor constants).
Reverse: unpack the nine conjuncts and feed them to yardstick_assignment_forced_from_cube_partition_principle, which already proves that any assignment obeying the role-kernel plus sum package equals the canonical pair. No further casework in this wrapper.
why it matters
Closes the O1' uniqueness surface in iff form: the canonical yardstick is not merely one survivor of the choice-set enumeration, but is definitionally equivalent to the cube-partition role-kernel plus structural-sum principle package. That package is the combinatorial content of the mass-ladder yardstick in the RS mass formula (yardstick times $\varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$).
The module doc states that valid choice sets collapse to singletons under these constraints; this theorem is the clean external interface to that collapse. No downstream consumers are wired yet in the graph, so it currently stands as a terminal uniqueness lemma for the Verification yardstick stack, ready to be cited by any later mass-spectrum or anchor-consistency argument that needs "the" power and $r_0$ assignment.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.