r0_depth_gap_iff_ew_role_under_affine_roles_and_sum
plain-language theorem explainer
Under fixed affine formulas for the up and down sector rungs and a fixed four-sector structural sum, the depth-gap condition (lepton rung minus electroweak rung equals W−10) is equivalent to pinning the electroweak rung to its canonical affine role 3W+4. Anyone tracing the unrestricted r0 forcing route cites this biconditional. The proof evaluates the affine roles to concrete integers and solves the resulting two-variable linear system both ways.
Claim. Let $a$ assign integer rungs 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{up}}+a_{\mathrm{down}}+a_{\mathrm{ew}}$ equals the structural $r_0$ sum target. Then $a_{\mathrm{lepton}}-a_{\mathrm{ew}}=W-10$ if and only if $a_{\mathrm{ew}}=3W+4$.
background
This module treats O1 yardstick assignment as a finite combinatorial search: four candidate $r_0$ values are permuted across the lepton, up, down, and electroweak sectors, then filtered by structural constraints until the valid choice set collapses to a singleton.
An $r_0$ assignment is simply a 4-tuple of integers, one rung per sector. The structural sum target is the fixed integer that all four rungs must add to (here 147). The affine up and down roles express those two rungs in terms of the window parameter $W$, the gap constant $A$, and the total excitation $E_{\mathrm{total}}$, so only lepton and electroweak remain free once the sum is imposed.
The depth gap is the integer difference between the lepton and electroweak rungs. The canonical electroweak affine formula is $3W+4$. The theorem equates those two residual conditions once up, down, and the sum are locked.
proof idea
Rewrite the sum hypothesis via the lemma that the $r_0$ sum target equals 147. Evaluate the up-role hypothesis to $a_{\mathrm{up}}=35$ and the down-role hypothesis to $a_{\mathrm{down}}=-5$ by native_decide on the fixed constants. Linear arithmetic then yields $a_{\mathrm{lepton}}+a_{\mathrm{ew}}=117$.
Both directions of the biconditional are elementary two-variable solves. Forward: the depth-gap hypothesis evaluates to difference 7, so electroweak equals 55, which matches $3W+4$. Reverse: the electroweak-role hypothesis evaluates to 55, so lepton equals 62 and the gap is 7, which matches $W-10$. Each numeric identity is discharged by native_decide or nlinarith.
why it matters
This biconditional is the bridge step in the alternate unrestricted forcing route. The sole downstream consumer assumes the affine up/down roles, the electroweak affine role, and the structural sum, then concludes the assignment equals the canonical $r_0$ 4-tuple; the present lemma converts a depth-gap hypothesis into that electroweak role (or conversely), so either residual condition finishes the force.
In the broader Recognition picture this sits inside yardstick assignment for the mass ladder (yardstick times $\varphi$ to a rung offset by the sector gap). Closing the $r_0$ choice set to a singleton is part of the O1 verification program: once sector rungs are forced, the phi-ladder mass formula has no remaining discrete ambiguity in those slots. The result does not itself invoke T5–T8, but it polices the integer skeleton those landmarks feed into when masses are read off.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.