listToR0Assignment
plain-language theorem explainer
Partial map from a four-integer list to an r0 sector assignment (lepton, up, down, electroweak). Returns none unless the list has exactly four entries. Downstream enumeration of the r0 choice set builds on it via filterMap over permutations of the candidate pool. The body is a two-clause pattern match.
Claim. Given a list of integers, return $\mathrm{Some}(a)$ where $a$ assigns the four entries in order to the lepton, up, down, and electroweak $r_0$ slots if and only if the list has length four; otherwise return $\mathrm{None}$.
background
The module treats the O1 yardstick discussion as a finite combinatorial search: start from four candidate $B_{\mathrm{pow}}$ values and four candidate $r_0$ values, enumerate all sector-to-value assignments (permutations), and filter by the structural constraints used in the yardstick argument. Valid choice sets collapse to singletons for both $B_{\mathrm{pow}}$ and $r_0$.
An $r_0$ assignment is a four-tuple of integers labeled lepton, up, down, and electroweak. The sibling structure R0Assignment is exactly that record (with Repr and DecidableEq). The names up and down echo the cosmological species labels (deconfined quarks with 12 DOF), but here they are only sector tags on the integer tuple.
This converter is the list-shaped entry point used when the candidate pool is permuted as raw List Int before being reified into typed assignments.
proof idea
Two-clause definition by pattern match. The singleton clause matches a four-element list $[l,u,d,e]$ and packs it into some { lepton := l, up := u, down := d, ew := e }. Every other list shape falls through to none. No lemmas are invoked.
why it matters
Feeds allR0Assignments, which is defined as r0ValuePool.permutations.filterMap listToR0Assignment?. That list is the raw choice set before structural and principle filters are applied, so the converter is the bridge from Mathlib permutations to the typed $r_0$ record used in the O1 collapse-to-singleton argument.
In the broader Recognition picture this sits inside verification of the yardstick mass formula (yardstick times $\varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$ on the phi-ladder). The module's claim is that once structural constraints are imposed, only one $r_0$ assignment survives; this def is the mechanical packing step that makes that enumeration type-check.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.