listToBPowAssignment
plain-language theorem explainer
Partial map from a four-integer list to a sector B-power assignment (lepton, up, down, electroweak). Enumeration code that builds the finite choice set of yardstick B_pow assignments cites it when turning permutations of the value pool into typed records. The definition is a single pattern match: length-four lists succeed, all other shapes return none.
Claim. Given a list of integers, return $\mathsf{some}$ sector $B_{\mathrm{pow}}$ assignment with fields $(\ell,u,d,e)$ when the list is exactly $[\ell,u,d,e]$; otherwise return $\mathsf{none}$.
background
The module treats the O1 yardstick discussion as a finite combinatorial search: four candidate $B_{\mathrm{pow}}$ values and four candidate $r_0$ values are assigned to sectors by enumerating permutations and filtering structural constraints. Valid choice sets collapse to singletons under those filters.
A $B_{\mathrm{pow}}$ assignment is a four-field integer record: lepton, up-quark, down-quark, and electroweak sector exponents. The up and down labels align with the deconfined quark species used elsewhere in the cosmology thresholds (each carrying 12 degrees of freedom), but here they are only sector tags for the yardstick exponents.
This converter is the bridge from raw integer lists (as produced by list permutations of the value pool) to that typed record.
proof idea
Definition by pattern match, not a proof. On input shape $[l,u,d,e]$ it returns $\mathsf{some}{\mathrm{lepton}:=l,\mathrm{up}:=u,\mathrm{down}:=d,\mathrm{ew}:=e}$. Every other list length or shape returns $\mathsf{none}$. No lemmas are invoked.
why it matters
Feeds allBPowAssignments, which builds the full candidate list as permutations of the $B_{\mathrm{pow}}$ value pool filtered through this map. That enumeration is the explicit O1 choice-set machinery: after structural and principle constraints, the surviving $B_{\mathrm{pow}}$ assignments collapse to a singleton, matching the yardstick uniqueness claim in the verification layer.
In the broader Recognition framework this sits under mass-yardstick bookkeeping on the $\varphi$-ladder (masses as yardstick times $\varphi$ to a rung offset). It does not itself force $\varphi$ or the rung formula; it only makes the finite sector-to-exponent search machine-checkable so the uniqueness filter can be stated without hand-waving over permutations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.