B_pow_formula_identities
plain-language theorem explainer
Each sector's binary power equals a fixed cube-edge formula: lepton −2E_passive, up quark −A, down quark 2E_total−1, electroweak +A. Cite when unpacking the yardstick table or sector mass exponents without unfolding B_pow by hand. Proof is four definitional simplifications of the sector cases.
Claim. Writing $B_{\mathrm{pow}}$ for the sector binary-power map, $A$ for the active-edge count, and $E_{\mathrm{passive}}$, $E_{\mathrm{total}}$ for the passive and total edge counts of the recognition 3-cube, one has $B_{\mathrm{pow}}(\mathrm{lepton})=-2E_{\mathrm{passive}}$, $B_{\mathrm{pow}}(\mathrm{up})=-A$, $B_{\mathrm{pow}}(\mathrm{down})=2E_{\mathrm{total}}-1$, and $B_{\mathrm{pow}}(\mathrm{EW})=A$.
background
The Yardstick Assignment Principle module (Open Problem O1) asks why each particle sector inherits a specific binary power and rung offset from the counting layer. The local answer is sector-to-cube coupling: leptons couple to passive edges, up quarks and electroweak to the single active edge, and down quarks to the full edge set of the 3-cube.
$B_{\mathrm{pow}}$ is the derived integer exponent for each sector, coming from cube edge counting rather than free parameters. Upstream anchors fix $A:=1$ (active edges per tick), $E_{\mathrm{passive}}:=11$ (passive field edges), and $E_{\mathrm{total}}:=12$. The definition of $B_{\mathrm{pow}}$ is already the four formulas above (lepton $-22$, up $-1$, down $23$, EW $+1$).
These exponents enter the mass yardstick as powers of two that suppress or amplify the $\varphi$-ladder contribution by sector. The module notes the structural pairing $|B_{\mathrm{pow}}(\mathrm{lepton})|+|B_{\mathrm{pow}}(\mathrm{EW})|=23=B_{\mathrm{pow}}(\mathrm{down})$ and $|B_{\mathrm{pow}}(\mathrm{up})|=A$.
proof idea
Pure definitional discharge. Four nested constructor steps split the conjunction; each conjunct is closed by simp [B_pow], which rewrites the sector case of the @[simp] definition of $B_{\mathrm{pow}}$ to the corresponding edge-count expression. No arithmetic lemmas or external theorems are required.
why it matters
Locks the formula layer of the O1 yardstick table to the counting-layer constants $A$, $E_{\mathrm{passive}}$, and $E_{\mathrm{total}}$. Without this identity bundle, later numerical claims (e.g. $B_{\mathrm{pow}}$ values or their sum) would have to re-unfold the sector match each time. It sits beside the sibling value and sum lemmas in the same module and underwrites the narrative that binary shifts measure how much each sector's recognition boundary borrows from the cube edge network: heavy passive borrowing for leptons ($2^{-22}$), minimal active-edge shifts for up/EW ($2^{\pm 1}$), and total-edge amplification for down quarks ($2^{23}$).
In the broader RS mass story these exponents multiply the yardstick on the $\varphi$-ladder. No downstream consumers are wired yet (used_by empty), so the lemma is presently a verification hinge inside O1 rather than a bridge into a parent theorem. It does not itself solve O1 (why these couplings); it only freezes the formulas the principle must explain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.