B_pow_eq_alt
plain-language theorem explainer
B_pow equals its alternative expression B_pow_alt for every sector. Researchers verifying the parameter-free derivation of sector yardsticks from hypercube edge counts would cite this equality. The proof reduces to case analysis on the sector followed by simplification against the edge-count definitions.
Claim. For each sector $s$, $B(s) = B_alt(s)$, where $B(s)$ is the sector power derived from cube edge counting ($B = -2E_p$ for leptons, $B = -A$ for up quarks, $B = 2E_t - 1$ for down quarks, $B = A$ for electroweak) and $B_alt(s)$ is the matching explicit integer formula.
background
The module verifies that sector constants are derived from first principles using $D=3$, cube_edges$(D)=12$, active_edges_per_tick$=1$, passive_field_edges$=11$, and wallpaper_groups$=17$. Key definitions include $W_z = 17$, $A_z = 1$, $E_{tz} = 12$, $E_{pz} = 11$. The primary $B_pow$ is defined directly from these edge counts: leptons use $-2E_p$, up quarks use $-A$, down quarks use $2E_t-1$, and electroweak uses $A$. The alternative $B_pow_alt$ supplies the explicit integers that match those counts.
proof idea
Case analysis on the four sectors, followed by simplification using the definitions of $B_pow$, $B_pow_alt$, $E_passive$, $E_total$, $A$, passive_field_edges, cube_edges, active_edges_per_tick, $D$, $E_{pz}$, $E_{tz}$, and $A_z$.
why it matters
This equality confirms that the primary $B_pow$ definition, built from edge combinatorics, coincides with the alternative integer expressions. It supports the module claim that all sector constants trace back to $D=3$ and the hypercube without free parameters, closing a verification step before the mass ladder is applied.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.