up_ew_sign_duality
plain-language theorem explainer
The up-quark and electroweak sectors carry opposite B-power exponents of equal magnitude, encoding active-edge sign duality (borrowing versus lending on the cube). Anyone auditing the yardstick assignment constraints cites this equality. The proof is a one-line simplification against the closed forms B_pow(up) = -A and B_pow(EW) = +A.
Claim. The binary power assigned to the up-quark sector equals the negation of the binary power assigned to the electroweak sector: $B_{\mathrm{pow}}(\mathrm{up}) = -B_{\mathrm{pow}}(\mathrm{EW})$.
background
The Yardstick Assignment Principle (Open Problem O1) asks why each particle sector receives its specific $B_{\mathrm{pow}}$ and $r_0$ formulas from the counting layer. The answer is combinatorial: each sector couples to a distinct level of the 3-cube hierarchy. Up quarks couple to the active edge ($A=1$), so $B_{\mathrm{pow}}(\mathrm{up})=-A=-1$ (borrowing). Electroweak couples to the same active edge with opposite sign, so $B_{\mathrm{pow}}(\mathrm{EW})=+A=+1$ (lending).
The module records the full sector table: leptons at $-2E_p=-22$, down quarks at $2E-1=23$, and the two active-edge partners at $\pm 1$. Magnitude pairing is structural: $|B_{\mathrm{pow}}(\mathrm{up})|=A$ and the lepton-EW absolute values sum to the down-quark exponent. The $r_0$ side uses wallpaper depth $W=17$ with multipliers ${4,2,-1,3}$ that exhaust the vertex count $V=8$.
proof idea
One-line tactic proof. Unfold the two closed-form identities $B_{\mathrm{pow}}(\mathrm{UpQuark})=-A$ and $B_{\mathrm{pow}}(\mathrm{Electroweak})=+A$ via simp only; the equality $-A=-(+A)$ is then definitional. No further arithmetic or case analysis is required.
why it matters
This is the sign-duality half of the assignment constraints. Downstream, assignment_valid packages four structural checks; its first field is exactly this theorem (sign_duality := up_ew_sign_duality). Together with the lepton-EW complement to the down-quark exponent, vertex exhaustion of the wallpaper depths, and edge-exhaustion of the additive corrections, it certifies that the current sector-to-cube coupling table is internally consistent.
In the broader Recognition framework the result anchors Open Problem O1: the yardstick exponents are not free parameters but edge-coupling depths on the 3-cube (T8 forces $D=3$). The active-edge pair $\pm A$ is the minimal borrowing/lending duality; it sits beside the eight-tick octave and the $\varphi$-ladder mass formula as a discrete structural input rather than a fitted constant.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.