lepton_ew_complement_down
plain-language theorem explainer
Lepton and electroweak binary yardstick exponents form a complementary pair: their absolute values sum to the down-quark exponent (22 + 1 = 23). Anyone auditing the yardstick assignment principle (Open Problem O1) or the structural B_pow Boolean filters cites this identity. The proof is a short numerical reduction through the three sector closed forms.
Claim. The absolute values of the lepton and electroweak binary yardstick exponents sum to the down-quark exponent: $|B_{\mathrm{pow}}(\mathrm{lepton})| + |B_{\mathrm{pow}}(\mathrm{electroweak})| = B_{\mathrm{pow}}(\mathrm{down\ quark})$. Equivalently, with the cube-edge closed forms, $|-2E_{\mathrm{passive}}| + |A| = 2E_{\mathrm{total}}-1$, i.e. $22+1=23$.
background
The Yardstick Assignment Principle module addresses Open Problem O1: why each particle sector receives its specific binary-power and $r_0$ formulas from the counting layer. The organizing idea is that each sector couples to a distinct level of the 3-cube combinatorial hierarchy, and the yardstick formulas encode that coupling.
$B_{\mathrm{pow}}$ assigns an integer power-of-two offset per sector, derived from cube edge counting (not free parameters): lepton gets $-2E_{\mathrm{passive}}=-22$, electroweak gets $+A=+1$, and down quark gets $2E_{\mathrm{total}}-1=23$. Upstream closed forms B_pow_Lepton_eq, B_pow_Electroweak_eq, and B_pow_DownQuark_eq pin these integers by simplifying the edge-count definitions.
The module's key structural observation is that the four $B_{\mathrm{pow}}$ values partition into complementary magnitude pairs. This declaration is the primary pair: leptons borrow heavily from passive edges while electroweak contributes the single active-edge bit, and together they match the down-quark total-edge doubling.
proof idea
One short tactic proof. Rewrite with the three sector evaluations B_pow_Lepton_eq ($=-22$), B_pow_Electroweak_eq ($=1$), and B_pow_DownQuark_eq ($=23$). Then norm_num discharges the integer identity $|-22|+|1|=23$.
why it matters
This identity is one of the structural constraints that certify the current yardstick assignment. It is installed as the complement field of assignment_valid, and is reused by anchor_bpow_constraints_from_principle to prove that the anchor $B_{\mathrm{pow}}$ assignment satisfies the Boolean filter bpowStructuralConstraints (via a simpa transport into the assignment record).
In the Recognition framework it is a concrete algebraic witness for the sector↔cube coupling story of O1: leptons borrow $2\times 11$ passive-edge bits, electroweak contributes the active-edge bit $A=1$, and the sum exhausts the down-quark total-edge formula $2E-1=23$. It is not a fitted numerology step; it records how recognition boundaries borrow from the cube edge network. It does not by itself close O1, but it is a required link in the constraint package that any competing assignment must match.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.