B_pow_Electroweak_eq
plain-language theorem explainer
The electroweak sector is assigned B_pow value exactly one by the cube-edge counting rule. Boson mass formulas and electroweak parameter theorems cite this identity to fix the phi-exponent offset before ladder evaluation. The proof reduces by direct substitution of the sector definition together with the constant active-edge count.
Claim. Let $B$ map each sector to its integer offset derived from cube geometry at $D=3$. Then $B($Electroweak$) = 1$.
background
The module assembles parameter-free constants from D=3 cube geometry: total edges equal 12, passive edges equal 11, and active edges per tick equal 1. B_pow is the function that returns these integer offsets for each sector; its Electroweak clause simply returns the active-edge count A. Upstream, active_edges_per_tick is fixed at 1 by the T2 tick rule, and the local A abbreviation re-exports that same constant.
proof idea
The proof is a one-line wrapper. It applies simp to unfold the B_pow definition at the Electroweak case, substitutes the value of A, and finishes with norm_num on the resulting arithmetic.
why it matters
This identity supplies the B_pow component required by electroweak_sector_params and by z_pred_eq when the Z mass is assembled on the phi ladder. It closes one geometric step in the derivation chain that begins from cube edge counting and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.