up_ew_same_magnitude
plain-language theorem explainer
Up-quark and electroweak sectors carry binary power assignments of equal absolute value, both equal to the active-edge count A = 1. Anyone auditing the yardstick partition or the finite-choice filter on sector signs would cite this. The proof reduces via the two sector equalities to |-1| = |1| and closes by arithmetic.
Claim. The absolute values of the derived binary powers for the up-quark and electroweak sectors coincide: $|B_{\mathrm{pow}}(\mathrm{Up})| = |B_{\mathrm{pow}}(\mathrm{EW})|$. Explicitly both equal $A = 1$, so $|-1| = |1|$.
background
The Yardstick Assignment Principle (Open Problem O1) asks why each particle sector receives a specific $B_{\mathrm{pow}}$ and $r_0$ from the counting layer. The answer is framed as sector-to-cube coupling: each sector couples to a distinct level of the 3-cube hierarchy, and the yardstick formulas encode that coupling.
$B_{\mathrm{pow}}$ is the integer power of two attached to each sector, derived from cube edge counts rather than fitted. From the anchor definitions: up quark couples to the active edge and gets $B_{\mathrm{pow}}(\mathrm{Up}) = -A = -1$; electroweak also couples to the active edge and gets $B_{\mathrm{pow}}(\mathrm{EW}) = +A = +1$. Here $A$ is the active-edges-per-tick count, fixed at 1.
Upstream equalities B_pow_UpQuark_eq and B_pow_Electroweak_eq already discharge the two evaluations to $-1$ and $1$ respectively by unfolding $B_{\mathrm{pow}}$ and $A$.
proof idea
One-step tactic proof. Unfold with the two sector identities B_pow_UpQuark_eq ($B_{\mathrm{pow}}(\mathrm{Up}) = -1$) and B_pow_Electroweak_eq ($B_{\mathrm{pow}}(\mathrm{EW}) = 1$), then close $|-1| = |1|$ by norm_num. No further lemmas are required.
why it matters
This is one half of the module's key structural observation: the four $B_{\mathrm{pow}}$ values partition into equal-magnitude pairs. The other half is the lepton/down relation $|B_{\mathrm{pow}}(\mathrm{Lepton})| + |B_{\mathrm{pow}}(\mathrm{EW})| = 23 = B_{\mathrm{pow}}(\mathrm{Down})$. Together they show the binary shifts are not free parameters but borrow counts from the cube edge network (leptons borrow $2E_p = 22$ bits; quarks borrow only the active edge $A = 1$).
The sibling block immediately after this theorem records sign constraints used by the finite-choice filter, so the magnitude equality is the numerical backbone those sign lemmas sit on. Within O1 it pins the up/EW row of the sector-coupling table and supports the claim that yardsticks come from 3-cube combinatorics rather than phenomenology. No downstream theorems currently depend on it by name; it is a local verification lemma inside the assignment principle.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.