bpow_sum_target_matches_principle
plain-language theorem explainer
The structural B-power sum target equals the sum of the four sector anchor powers (lepton, up quark, down quark, electroweak). Anyone verifying that the choice-set filter agrees with the yardstick principle cites this bridge. The proof is a two-line calc equating both sides to 1 via the target-equals-one lemma and the principle sum identity.
Claim. The structural $B$-power sum target equals $B_{\mathrm{pow}}(\mathrm{lepton})+B_{\mathrm{pow}}(\mathrm{up})+B_{\mathrm{pow}}(\mathrm{down})+B_{\mathrm{pow}}(\mathrm{electroweak})$.
background
This module treats the O1 yardstick discussion as a finite combinatorial search: four candidate $B_{\mathrm{pow}}$ values and four $r_0$ values are assigned to sectors by permutation, then filtered by structural constraints. Valid choice sets collapse to singletons under those filters.
Sector $B_{\mathrm{pow}}$ values are derived powers of two from cube edge counting, not free parameters: lepton $-22$, up $-1$, down $23$, electroweak $+1$. The structural sum target is the counting-layer constant $A$ cast to $\mathbb{Z}$, which evaluates to $1$. Upstream, the yardstick principle already proves that the four sector powers sum to $1$.
proof idea
Two-step calc. First rewrite the sum target to $1$ by bpow_sum_target_eq_one (native decision on $A=1$). Then identify $1$ with the four-sector sum by symmetry of YardstickAssignmentPrinciple.B_pow_sum, which expands the sector formulas and closes by norm_num.
why it matters
Closes the gap between the choice-set filter's numeric sum target and the principle-layer identity that the anchor $B_{\mathrm{pow}}$ values sum to one. Downstream, anchor_bpow_structural_identities uses this match so each conjunct of the $B_{\mathrm{pow}}$ filter is witnessed by a proved structural identity from the yardstick principle (sign relations, absolute-value balance, ordering). That is the bridge that lets the enumerated choice set certify the anchor assignment rather than merely list candidates. Sits in the verification layer that makes O1 yardstick uniqueness a finite, checkable collapse.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.