bpow_sum_target_eq_one
plain-language theorem explainer
The structural sum target for sector B_pow values is the integer 1. Anyone filtering yardstick assignments by the sum constraint cites this equality. The proof is a one-line native decision on the definition of the target as the cast of the anchor constant A.
Claim. The structural $B_{\mathrm{pow}}$ sum target equals $1$ in $\mathbb{Z}$.
background
This module treats O1 yardstick assignment as a finite search: four candidate $B_{\mathrm{pow}}$ values and four $r_0$ values, all sector-to-value permutations, then structural filters. Valid choice sets collapse to singletons under those constraints.
The sum target is defined as the integer cast of the anchor constant $A$, documented as the structural $B_{\mathrm{pow}}$ sum target with $A = 1$. Assignments $a$ for lepton, up, down, and electroweak sectors are required to satisfy $a_{\ell}+a_u+a_d+a_{\mathrm{ew}}$ equal to that target in the principle and structural constraint packs.
Downstream forcing lemmas rewrite the four-term sum against this constant, often reducing via sign duality $a_u=-a_{\mathrm{ew}}$ to a two-term identity $a_{\ell}+a_d$ equal to the same target.
proof idea
One-line wrapper: native_decide evaluates the definition of the sum target as $(A:\mathbb{Z})$ and confirms it equals $1$. No intermediate lemmas are invoked.
why it matters
This pins the numerical value of the structural sum that every principle-constraint and forcing argument in the module uses. Immediate consumers include the match of the target to the canonical four-sector $B_{\mathrm{pow}}$ sum, the principle normal form (active-edge pair fixed, down $=1-$ lepton), unrestricted forcing from the down-role amplification, lepton forced from down-role plus sign sum, the equivalence of passive-edge lepton role and down-role under sign duality, and sign duality forced from lepton-down fixation.
In the broader Recognition picture this is bookkeeping for the yardstick mass ladder (sector $B_{\mathrm{pow}}$ exponents on the $\varphi$-ladder), not a new forcing step in T0–T8. It closes the O1 combinatorial claim that filtered assignments collapse once the sum is fixed at $1$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.