B_pow_values
plain-language theorem explainer
The four sector binary-exponent offsets are fixed: lepton −22, up quark −1, down quark 23, electroweak +1. Mass-ladder and yardstick-assignment arguments cite this as the concrete numerical content of the cube-edge B_pow map. The proof is a one-line packing of the four sector-wise evaluation lemmas.
Claim. The sector binary powers equal $B(\mathrm{lepton})=-22$, $B(\mathrm{up\ quark})=-1$, $B(\mathrm{down\ quark})=23$, and $B(\mathrm{electroweak})=1$.
background
The module treats Open Problem O1: why each particle sector receives a definite binary power and $r_0$ offset from the counting layer. The principle is that sectors couple to distinct levels of the 3-cube hierarchy (passive edges, active edge, total edges), and the yardstick formulas encode that coupling.
The map $B_{\mathrm{pow}}$ assigns an integer power of two per sector from cube edge counts: lepton $-(2 E_{\mathrm{passive}})=-22$, up quark $-A=-1$, down quark $2E_{\mathrm{total}}-1=23$, electroweak $+A=+1$. Upstream, each equality is already proved by simplifying the definition against the fixed combinatorial constants ($E_{\mathrm{passive}}=11$, $E_{\mathrm{total}}=12$, $A=1$, $D=3$).
Those four lemmas are the only inputs. The present statement merely packages them as a single conjunction for citation at the verification layer.
proof idea
Term-mode one-liner: the goal is a four-way conjunction, so the proof is the 4-tuple of the existing sector lemmas B_pow_Lepton_eq, B_pow_UpQuark_eq, B_pow_DownQuark_eq, and B_pow_Electroweak_eq. Each of those lemmas is itself a simp of the B_pow definition against the cube-edge constants followed by norm_num. No new arithmetic is done here.
why it matters
This is the numerical anchor for the B_pow column of the Yardstick Assignment Principle (O1). The module records the structural partition $|B(\mathrm{lepton})|+|B(\mathrm{EW})|=23=B(\mathrm{down})$ and $|B(\mathrm{up})|=A=1$, read as binary shifts that measure how much each sector's recognition boundary borrows from the cube edge network (leptons $2^{-22}$ suppression; quarks $2^{\pm 1}$; down $2^{23}$ amplification).
In the broader RS mass formula, yardstick times $\varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$ sits on the phi-ladder; these integer powers supply the sector-dependent binary prefactors that feed that ladder. The declaration sits in Verification rather than Masses.Anchor so that O1 can quote a single proved bundle. No downstream users are wired yet; sibling results (B_pow_sum, B_pow_sum_eq_A, complement identities) build the same numerical story for the sum and pairing claims.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.