canonicalR0
plain-language theorem explainer
The canonical integer r0 assignment for the four mass sectors (lepton, up, down, electroweak), written in terms of the anchor width W, active-edge count A, and total cube edges. Anyone proving uniqueness of yardstick r0 assignments cites this as the forced target. The body is a pure structure literal: four affine formulas, no proof obligations.
Claim. The canonical $r_0$ assignment is the four-tuple of integers $(r_\ell, r_u, r_d, r_{\mathrm{EW}}) = (4W - 6,\, 2W + A,\, E_{\mathrm{tot}} - W,\, 3W + 4)$ for the lepton, up, down, and electroweak sectors, where $W$ is the anchor width, $A$ is the active-edge count per tick, and $E_{\mathrm{tot}}$ is the total number of cube edges.
background
This module turns the O1 yardstick discussion into a finite combinatorial search: enumerate all sector-to-value assignments of candidate $B_{\mathrm{pow}}$ and $r_0$ integers, then filter by the structural constraints used in the yardstick principle. Valid choice sets are claimed to collapse to singletons for both quantities.
An $r_0$ assignment is a four-tuple of integers, one per sector (lepton, up, down, electroweak). The anchor constants entering the formulas are standard: $A$ is the active-edge count per tick (equal to 1), and $E_{\mathrm{tot}}$ is the total cube-edge count in spatial dimension $D=3$ (equal to 12). The width parameter $W$ is the remaining free integer scale from the mass-anchor layer.
The four formulas are the affine role assignments that later uniqueness theorems treat as either hypotheses or derived equalities: up and down fixed by $W$ and the edge counts, electroweak by a second affine role in $W$, and lepton by the remaining affine expression.
proof idea
No proof: this is a structure literal. The four fields of the $r_0$-assignment record are filled by the closed-form integer expressions $4W-6$, $2W+A$, $E_{\mathrm{tot}}-W$, and $3W+4$. Downstream uniqueness arguments compare an arbitrary assignment against this record by native_decide or by algebraic cancellation under the role and sum hypotheses.
why it matters
This record is the singleton target of the O1 choice-set collapse for $r_0$. Downstream, anchor_r0_matches_canonical checks that the anchor-side assignment equals this one by decision procedure. The family r0_constraints_force_canonical, r0_unrestricted_forcing_from_affine_roles, and r0_unrestricted_forcing_from_affine_roles_and_ew_role all conclude equality with this canonical tuple once affine up/down roles, depth gap (or EW role), and the structural sum are imposed.
Equivalence forms such as r0_principle_iff_sum_under_affine_roles_and_depth_gap reduce the full principle constraints to the sum target alone under those roles, with this definition supplying the concrete values the sum forces. In the broader RS picture the $r_0$ integers sit inside the mass yardstick on the $\varphi$-ladder (rung offset relative to the eight-tick octave), so pinning the sector assignment is a verification step toward a unique mass formula rather than a free combinatorial choice.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.