B_pow_alt
plain-language theorem explainer
B_pow_alt supplies an alternative case-by-case expression for the sector exponent B_pow using the derived integers Epz (passive field edges), Az (active edges per tick), and Etz (cube edges). Mass-spectrum workers in Recognition Science cite it to cross-check the parameter-free yardstick derivation from D=3 cube combinatorics and wallpaper groups. The definition is exhaustive case analysis on the four Sector constructors, directly substituting the precomputed constants.
Claim. Define the function $B(s)$ on sectors $s$ by $B($Lepton$)=-2p$, $B($UpQuark$)=-a$, $B($DownQuark$)=2e-1$, $B($Electroweak$)=a$, where $p$ is the number of passive field edges, $a$ the number of active edges per tick, and $e$ the total number of cube edges (all evaluated at spatial dimension $D=3$).
background
The AnchorDerivation module verifies that sector constants arise directly from first principles. It defines Epz as passive_field_edges(D), Az as active_edges_per_tick, and Etz as cube_edges(D). With D=3 these evaluate to 11, 1 and 12 respectively. The inductive type Sector has four constructors: Lepton, UpQuark, DownQuark, Electroweak. The module documentation states that all sector constants trace back to D=3, cube_edges(D)=12, active_edges_per_tick=1, passive_field_edges=11 and wallpaper_groups=17, with no free parameters.
proof idea
This is a definition by cases on the Sector inductive type. Each branch substitutes the sibling constants Epz, Az or Etz into the listed arithmetic expression, reproducing the numerical values shown in the module table (Lepton yields -22, UpQuark yields -1, etc.). No tactics or lemmas are applied; the body is the direct pattern match.
why it matters
B_pow_alt is invoked by the downstream theorem B_pow_eq_alt, which proves syntactic equality with the primary Anchor.B_pow. It thereby closes the verification that the sector exponents are derived from cube geometry and the wallpaper constant 17, supporting the claim of a parameter-free mass ladder. The construction rests on the T8 forcing of D=3 and the cube-edge counting that yields the missing-11 passive edges.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.