r0_unrestricted_forcing_from_affine_roles
plain-language theorem explainer
Under affine up/down sector roles and a fixed lepton–electroweak depth gap, the full r0 principle constraints force any integer sector assignment to equal the canonical r0 values. Anyone auditing uniqueness of the yardstick rung-zero choice set (without finite-pool membership) would cite this. The proof is a short reduction: order conjuncts are discarded and the sum-only unrestricted forcing lemma is applied.
Claim. Let $a$ assign integers to the lepton, up, down, and electroweak sectors. Suppose $a_{\mathrm{up}} = 2W + A$, $a_{\mathrm{down}} = E_{\mathrm{total}} - W$, and $a_{\mathrm{lepton}} - a_{\mathrm{ew}} = W - 10$. If $a$ also satisfies the full r0 principle constraints (sign/order inequalities plus the structural sum target), then $a$ equals the canonical r0 assignment.
background
This module treats the O1 yardstick discussion as a finite combinatorial search: candidate $B_{\mathrm{pow}}$ and $r_0$ values are assigned to the four sectors (lepton, up, down, electroweak), then filtered by structural constraints until the valid choice sets collapse to singletons.
An R0Assignment is simply four integers, one per sector. The affine role hypotheses pin the up and down entries to linear forms in the conditional gravity weight $W$ and the active-edge count $A$ (from the gap derivation, $A = 1$), together with a total-energy offset $E_{\mathrm{total}}$. The depth-gap hypothesis fixes the lepton–electroweak difference as $W - 10$.
The principle-constraint bundle packages the usual order inequalities (down negative, lepton above electroweak, electroweak above up) with the structural sum target that the four sector values must meet. The theorem asserts that, once the affine roles and depth gap are fixed, that whole bundle already forces the canonical assignment—no separate finite-pool membership test is required.
proof idea
Term-mode one-step reduction. Destructure the principle-constraint hypothesis into its four conjuncts (down-negative, lepton $>,$ electroweak, electroweak $>,$ up, and the sum target). Discard the three order conjuncts and feed the remaining sum hypothesis, together with the three affine/depth-gap hypotheses, into the already-proved lemma that unrestricted forcing holds from affine roles plus the sum alone. That lemma returns equality with the canonical r0 assignment.
why it matters
In the Recognition mass formula the yardstick multiplies a $\varphi$-ladder term $\varphi^{r-8+\mathrm{gap}(Z)}$. The integer $r_0$ sector offsets are part of that ladder bookkeeping; if they were free, the mass spectrum would not be unique. This theorem closes the unrestricted (no finite-pool) half of the O1 uniqueness argument: affine up/down roles plus the depth gap already pin $r_0$ to the canonical values once the principle constraints hold.
The companion observation in the module is that, under those same affine roles, the full principle bundle is equivalent to the structural sum target alone—the order inequalities become derived. Together these results justify treating the r0 choice set as a singleton in the yardstick verification chain, parallel to the $B_{\mathrm{pow}}$ singleton collapse. No downstream consumers are wired yet; the result stands as a leaf uniqueness certificate inside the verification layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.