bpow_principle_normal_form
plain-language theorem explainer
Under the B_pow principle constraints, any integer sector assignment is forced into a normal form: the electroweak rung is +1, the up rung is −1, the down rung equals 1 minus the lepton rung, and the lepton rung is nonpositive. Mass-ladder and yardstick auditors cite this when collapsing the free B_pow choice set. The proof is pure integer arithmetic: absolute-value identities plus nlinarith from the sign, composition, positivity, and sum constraints.
Claim. Let $a$ be an integer assignment of $B_{\mathrm{pow}}$ rungs to the lepton, up, down, and electroweak sectors. If $a$ satisfies the $B_{\mathrm{pow}}$ principle constraints (sign pairing, composition/absolute-value relation, electroweak positivity, and the fixed sum target), then $a_{\mathrm{ew}}=1$, $a_{\mathrm{up}}=-1$, $a_{\mathrm{down}}=1-a_{\mathrm{lepton}}$, and $a_{\mathrm{lepton}}\le 0$.
background
This module treats the O1 yardstick discussion as a finite combinatorial search: four candidate $B_{\mathrm{pow}}$ values and four candidate $r_0$ values are assigned to sectors by permutation, then filtered by structural and principle constraints. Valid choice sets collapse to singletons for both $B_{\mathrm{pow}}$ and $r_0$.
A $B_{\mathrm{pow}}$ assignment is a 4-tuple of integers (lepton, up, down, ew). The principle constraints (destructured in the proof) encode: a sign relation linking up and ew, a composition identity equating the down value to a sum of absolute values on lepton and ew, strict positivity of the electroweak coordinate, and a sum constraint whose target equals 1 (via the sibling fact that the $B_{\mathrm{pow}}$ sum target is one).
In the broader RS mass picture, $B_{\mathrm{pow}}$ enters the yardstick that scales the $\varphi$-ladder mass formula. Normalizing the free integer assignment is the algebraic step before matching the canonical anchor formulas.
proof idea
Tactic proof by integer arithmetic, no external RS lemmas beyond the local sum-target identity.
Destructure the principle bundle into sign, composition, ew-positivity, and sum. From sum and sign, obtain lepton + down = bpowSumTarget, then rewrite by bpow_sum_target_eq_one to get sum 1. Rewrite composition as |lepton| + |ew| = down. Positivity of ew gives |ew| = ew, so lepton + |lepton| + ew = 1.
Since ew is a positive integer, ew ≥ 1, hence lepton + |lepton| ≤ 0. Combined with 2·lepton ≤ lepton + |lepton| (from le_abs_self), conclude lepton ≤ 0, so |lepton| = -lepton. Substitute back to force ew = 1. Sign then forces up = -1, and the sum identity gives down = 1 - lepton. Package the four conjuncts.
why it matters
This is the algebraic normal-form step inside the O1 yardstick choice-set program: principle constraints alone, without finite-pool membership, pin three of the four $B_{\mathrm{pow}}$ coordinates and the sign of the fourth. The module doc states that valid assignments collapse to singletons; this theorem supplies the unrestricted forcing shape that makes that collapse inevitable once the lepton sector is chosen.
The immediately following module comment records the intended payoff: once the lepton sector is fixed to passive-edge coupling $-2E_p$, the same constraints force the full canonical $B_{\mathrm{pow}}$ assignment. That canonical form feeds the yardstick in the $\varphi$-ladder mass formula (yardstick $\cdot \varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$).
No downstream Lean users are wired yet (used_by empty), so the result is presently a verification lemma awaiting the unrestricted-forcing corollary and the singleton-collapse theorems for the enumerated choice sets.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.