bpow_pool_matches_anchor_formulas
plain-language theorem explainer
The candidate integer pool used in yardstick B_pow assignment search is definitionally the ordered list of sector powers from the mass anchor: lepton, up-quark, down-quark, electroweak. Anyone auditing that the O1 choice-set enumeration starts from the cube-edge formulas would cite this. The proof is pure reflexivity of the two list definitions.
Claim. The yardstick power pool equals $[B_{\mathrm{pow}}(\mathrm{lepton}),\, B_{\mathrm{pow}}(\mathrm{up}),\, B_{\mathrm{pow}}(\mathrm{down}),\, B_{\mathrm{pow}}(\mathrm{EW})]$, where each $B_{\mathrm{pow}}$ is the sector power derived from cube-edge counting.
background
In the mass-anchor layer, each Standard Model sector carries a derived integer power $B_{\mathrm{pow}}$ coming from cube edge counting, not free parameters: lepton $\mapsto -(2 E_{\mathrm{passive}})=-22$, up-quark $\mapsto -A=-1$, down-quark $\mapsto 2E_{\mathrm{total}}-1=23$, electroweak $\mapsto A=1$.
This module turns the O1 yardstick discussion into a finite combinatorial search: take the four candidate $B_{\mathrm{pow}}$ values and the four candidate $r_0$ values, enumerate sector-to-value assignments, and filter by structural constraints. The pool list is the raw multiset of those four integers before any permutation is applied.
The theorem simply identifies that pool with the ordered evaluation of the anchor formulas on the four sectors.
proof idea
One-line reflexivity. The pool is defined as the list of the four arithmetic expressions that appear in the cases of $B_{\mathrm{pow}}$, in the same sector order (lepton, up, down, electroweak). Unfolding both sides yields identical List ℤ terms, so rfl closes the goal.
why it matters
O1 progress in the verification layer requires that the choice-set search start from the same integers the mass anchor already fixes. Without this equality, the enumerated assignments could drift from the cube-edge formulas and the later collapse to a singleton $B_{\mathrm{pow}}$ assignment would be unanchored.
Sibling results (bpow_sum_target_matches_principle, structural and principle constraint filters, allBPowAssignments) consume the pool; this lemma pins the pool to the anchor before those filters run. It is bookkeeping rather than new physics, but it is the definitional bridge between Masses.Anchor and the combinatorial O1 search. No downstream theorem currently depends on it by name; it is infrastructure for the choice-set uniqueness claim in the module doc.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.