anchor_is_unique_valid_bpow
plain-language theorem explainer
The anchor sector-to-power map lies in the structurally valid B_pow assignment list. Anyone verifying that the RS mass yardstick uses the unique admissible power assignment would cite this. Proof is a two-step rewrite: the valid list equals the singleton of the canonical assignment, and the anchor map equals that canonical one, so membership is immediate.
Claim. The sector assignment of $B_{\mathrm{pow}}$ values read from the mass-anchor formulas belongs to the finite list of all $B_{\mathrm{pow}}$ assignments that pass the structural yardstick constraints.
background
The module treats the O1 yardstick discussion as a finite combinatorial search. Four candidate $B_{\mathrm{pow}}$ values are assigned to the four sectors (lepton, up-quark, down-quark, electroweak) in all permutations; structural constraints then filter the list. Under those constraints the valid choice set collapses to a singleton.
The anchor assignment is the map that reads each sector's $B_{\mathrm{pow}}$ from the corresponding anchor formula. A separate native-decision lemma identifies that map with the canonical survivor of the filter. The valid list itself is defined as the full enumeration filtered by the structural predicate, and is proved equal to the one-element list containing only the canonical assignment.
proof idea
Short rewrite proof. Rewrite the membership goal using the singleton theorem (valid assignments equal [canonical]) and the identification of the anchor map with the canonical assignment. The resulting goal is membership of an element in the singleton list of itself, discharged by simp.
why it matters
Closes the O1 checkpoint that the physical anchor $B_{\mathrm{pow}}$ values are exactly the unique structurally admissible assignment produced by the choice-set enumeration. That uniqueness is the combinatorial half of the yardstick story behind the mass formula (yardstick times a $\phi$-ladder factor). No downstream theorems currently depend on it; it stands as a verification seal that the RS-native sector powers are forced by the filter rather than freely chosen. Complements the parallel $r_0$ singleton result in the same module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.