up_negative_and_ew_positive
plain-language theorem explainer
The up-quark sector power is strictly negative and the electroweak power is strictly positive. Anyone filtering admissible yardstick assignments by sign pattern cites this. The proof unfolds the two closed-form equalities and finishes by numeric evaluation.
Claim. Writing $B_{\mathrm{pow}}$ for the integer cube-edge power assigned to each particle sector, one has $B_{\mathrm{pow}}(\mathrm{Up}) < 0$ and $B_{\mathrm{pow}}(\mathrm{EW}) > 0$.
background
The Yardstick Assignment Principle module treats Open Problem O1: why each particle sector receives a definite integer power $B_{\mathrm{pow}}$ (and offset $r_0$) from the 3-cube counting layer. Sectors couple to distinct levels of the cube hierarchy. The power map is defined by edge counts: up quark gets $-A = -1$ (active edge), electroweak gets $+A = +1$, lepton gets $-2E_{\mathrm{passive}} = -22$, and down quark gets $2E_{\mathrm{total}}-1 = 23$.
As the module notes, the powers partition into equal-magnitude pairs, and the binary shifts encode how much each sector's recognition boundary borrows from the cube edge network. The present statement isolates only the sign half of that structure for the up and electroweak sectors.
Upstream, B_pow is the sector-indexed integer definition in Masses.Anchor, with simp lemmas B_pow_UpQuark_eq and B_pow_Electroweak_eq exposing the concrete values $-1$ and $+1$.
proof idea
Term-mode proof in two steps. First simp only rewrites both sides via the closed equalities $B_{\mathrm{pow}}(\mathrm{Up}) = -1$ and $B_{\mathrm{pow}}(\mathrm{EW}) = 1$. Then norm_num discharges the elementary inequalities $-1 < 0$ and $0 < 1$. No further lemmas are required.
why it matters
This is one of the sign constraints that appear in the finite-choice filter on yardstick assignments. Downstream, anchor_bpow_structural_identities packages the full $B_{\mathrm{pow}}$ filter: opposite signs for up and electroweak, the lepton/EW absolute-value sum equaling the down power, and the two strict inequalities proved here. The parent theorem states that the anchor assignment satisfies every conjunct of that filter.
In the Recognition framework this sits inside O1 (sector-to-cube coupling). The opposite signs for up and electroweak both equal $\pm A$ with $A=1$ are the minimal edge-borrow case in the module table, complementary to the heavy lepton suppression $2^{-22}$ and the down amplification $2^{23}$. The result is pure integer arithmetic on the counting layer; it does not itself derive masses, but it licenses the admissible power pattern used by the mass yardstick on the $\varphi$-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.