lepton_ew_natAbs_complement_down
plain-language theorem explainer
The absolute values of the lepton and electroweak binary power exponents sum to the down-quark exponent: |B_pow(Lepton)| + |B_pow(EW)| = B_pow(Down). Anyone checking the Boolean B_pow filter on the anchor assignment cites this cast form. The proof unfolds the three sector equalities and finishes by numeric evaluation.
Claim. Casting absolute values to integers, $|B_{\mathrm{pow}}(\mathrm{Lepton})| + |B_{\mathrm{pow}}(\mathrm{Electroweak})| = B_{\mathrm{pow}}(\mathrm{DownQuark})$. With the sector values $-22$, $+1$, and $23$, this is $22 + 1 = 23$.
background
Open Problem O1 asks why each particle sector receives a fixed binary power $B_{\mathrm{pow}}$ from the 3-cube counting layer. The Yardstick Assignment Principle ties sectors to cube coupling levels: leptons to passive edges ($B_{\mathrm{pow}} = -2E_p = -22$), electroweak to the active edge ($B_{\mathrm{pow}} = +A = +1$), and down quarks to total edges ($B_{\mathrm{pow}} = 2E-1 = 23$). Here $A = 1$ is the active-edge count per tick.
A structural observation in the module is that the $B_{\mathrm{pow}}$ values partition into equal-magnitude pairs. In particular $|B_{\mathrm{pow}}(\mathrm{Lepton})| + |B_{\mathrm{pow}}(\mathrm{EW})| = 22 + 1 = 23 = B_{\mathrm{pow}}(\mathrm{Down})$. The present theorem is the Int.natAbs cast of that identity, the form demanded by Boolean filter constraints on the anchor assignment.
Sibling lemmas supply the concrete equalities $B_{\mathrm{pow}}(\mathrm{Lepton}) = -22$, $B_{\mathrm{pow}}(\mathrm{EW}) = 1$, and $B_{\mathrm{pow}}(\mathrm{Down}) = 23$, together with the non-cast complement lepton_ew_complement_down.
proof idea
Term-mode proof in two steps. First simp only rewrites the three sector powers via B_pow_Lepton_eq, B_pow_Electroweak_eq, and B_pow_DownQuark_eq, replacing the symbolic sector arguments by the integers $-22$, $1$, and $23$. Then norm_num evaluates Int.natAbs and the integer sum, closing $22 + 1 = 23$. No external lemmas beyond those three equalities are required.
why it matters
This identity is one of the four conjuncts that anchor_bpow_structural_identities (in YardstickAssignmentChoiceSet) demands of the anchor $B_{\mathrm{pow}}$ assignment: the filter requires
$((\mathrm{natAbs},\mathrm{lepton}:\mathbb{Z}) + (\mathrm{natAbs},\mathrm{ew}:\mathbb{Z}) = \mathrm{down})$
alongside the up/EW sign and magnitude relations. Discharging it shows the combinatorial yardstick table is not an ad-hoc fit but satisfies the Boolean constraints used downstream in verification.
In the broader RS picture the exponents sit on the $\varphi$-ladder mass formula (yardstick $\cdot \varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$). The 22-bit lepton suppression and the 23-bit down amplification are the binary shifts that encode how much each sector borrows from the cube edge network. Closing this cast form is a small but necessary step toward resolving O1: why the counting layer forces these particular sector powers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.