R0Assignment
plain-language theorem explainer
Four-sector integer record for the r0 yardstick offsets: lepton, up, down, and electroweak. The O1 choice-set enumeration builds every permutation of the r0 value pool into this type, then filters by structural sum and role constraints. Parallel to the B_pow assignment record; pure data with decidable equality, no proof content.
Claim. An $r_0$ assignment is a 4-tuple of integers $(r_0^{\ell},\, r_0^{u},\, r_0^{d},\, r_0^{\mathrm{EW}})$ assigning one integer offset to each of the lepton, up-quark, down-quark, and electroweak sectors.
background
The module treats the O1 yardstick discussion as a finite combinatorial search. One starts from a fixed pool of four candidate $r_0$ integers and four candidate $B_{\mathrm{pow}}$ integers, forms every sector-to-value assignment (all permutations), and retains only those that satisfy the structural constraints used in the yardstick principle. Valid choice sets collapse to singletons for both $B_{\mathrm{pow}}$ and $r_0$.
This structure is the $r_0$ half of that bookkeeping. It mirrors BPowAssignment: four integer fields, one per sector (lepton, up, down, electroweak), with derived printable and decidable-equality instances so the filter can be run as ordinary boolean computation. Downstream, the canonical formulas fix the four components in terms of the yardstick constants $W$, $A$, and $E_{\mathrm{total}}$ (e.g. lepton $= 4W-6$, up $= 2W+A$).
proof idea
No proof: a structure declaration. Four fields of type $\mathbb{Z}$, deriving Repr and DecidableEq so assignments can be printed and compared in the enumeration filter. Construction sites pack four-element lists via the optional list converter, or write the four components explicitly as in the canonical and anchor instances.
why it matters
Carrier type for the entire $r_0$ branch of the O1 choice-set argument. Every permutation of the $r_0$ value pool is reified as an assignment; structural and principle constraints are predicates on this type; and the forcing theorems (boolean filter under affine up/down roles plus depth gap, sum-target equivalence, and the forced-true form) all quantify over it.
Downstream parents include the full enumeration list, the list-to-assignment converter, the canonical closed-form assignment, the anchor readout from the mass ladder, and the boolean constraint lemmas that prove the filtered set is a singleton. That singleton is the unique $r_0$ sector map compatible with the yardstick principle, feeding the mass formula (yardstick $\cdot \varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$) on the $\varphi$-ladder. Closes the combinatorial half of O1 for $r_0$ the same way the parallel $B_{\mathrm{pow}}$ structure closes it for powers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.