yardstick_choice_sets_collapsed
plain-language theorem explainer
Under the O1 structural filters on sector-to-value maps, the admissible B-power assignments and the admissible r0 assignments each collapse to a single list entry: the canonical choice. Anyone checking that the yardstick layer is uniquely fixed by the current constraint set cites this. The proof is a one-line pairing of the two singleton lemmas already proved for each layer.
Claim. The filtered list of valid $B_{\mathrm{pow}}$ sector assignments equals the singleton list containing only the canonical $B_{\mathrm{pow}}$ assignment, and the filtered list of valid $r_0$ sector assignments equals the singleton list containing only the canonical $r_0$ assignment.
background
This module turns the O1 yardstick discussion into an explicit finite search. One starts from four candidate $B_{\mathrm{pow}}$ values and four candidate $r_0$ values, forms all sector-to-value assignments (permutations), and retains only those that satisfy the structural constraints used in the yardstick analysis (sum targets, role-kernel shape, and related filters from the assignment principle).
The mass yardstick sits on the $\varphi$-ladder: particle masses are written as a yardstick times $\varphi$ raised to a rung offset with a charge-dependent gap. Here the combinatorial layer asks which discrete assignments of the $B_{\mathrm{pow}}$ and $r_0$ parameters to sectors survive those filters. Canonical assignments are the distinguished survivors; mirrored or other pool members are candidates that the filters must rule out.
Upstream, the assignment principle and anchor formulas fix the numerical pool and the sum-to-one style targets that the filters encode. The present theorem only packages the two already-established singleton collapses into one joint statement.
proof idea
Term-mode pairing. The goal is a conjunction of two equalities of lists. Apply the existing lemma that every valid $B_{\mathrm{pow}}$ assignment list equals the singleton of the canonical $B_{\mathrm{pow}}$ assignment, and the parallel lemma that every valid $r_0$ assignment list equals the singleton of the canonical $r_0$ assignment. No further case analysis or enumeration happens at this site.
why it matters
In the Recognition Science mass story, the yardstick and the discrete rung structure must not leave free combinatorial choice once the structural sums and role-kernel assumptions are imposed. This declaration is the O1 enumerated-choice closure summary: both yardstick layers reduce to unique canonical assignments under the current constraint set.
It records that the finite search described in the module really does collapse, so later verification steps can treat the canonical $B_{\mathrm{pow}}$ and canonical $r_0$ maps as forced rather than as one option among many. The nearby joint-forcing remark stresses the intended reading: once cube-role couplings are fixed, role-kernel assumptions plus structural sums force both layers without needing a full filter-bundle hypothesis.
No downstream consumers are wired yet in the graph; the result is a verification checkpoint for the O1 progress claim rather than an input to a named parent theorem. It sits beside the mass-formula landmarks (yardstick, $\varphi$-ladder, rung offsets) without touching T5–T8 directly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.