N_sec_eq
plain-language theorem explainer
The equality fixes the fermion sector count at four once spatial dimension equals three. Researchers deriving lepton masses on the phi-ladder cite it to anchor the binary gauge before computing B and r0. The proof is a one-line unfolding of the sector definition followed by arithmetic normalization.
Claim. With spatial dimension $D=3$, the number of fermion sectors satisfies $N_ {sec} := 2^{D-1} = 4$.
background
In the T9 electron mass module the lepton sector constants are derived from cube geometry rather than postulated. The sibling definition states $N_{sec} := 2^{D-1}$, which counts the fermion sectors once the spatial dimension is fixed at three. This count enters the binary exponent $B = -(2 E_{passive})$ and the rung offset $r_0 = 4W - (8 - r_{baseline})$ that later fix the electron mass on the phi-ladder.
proof idea
The proof is a one-line wrapper that unfolds the definition of $N_{sec}$ together with the dimension $D$ and then applies numerical normalization to the resulting power.
why it matters
The result anchors the sector count inside the electron mass derivation chain that begins from cube edges, passive field count eleven, and the eight-tick octave. It precedes the lepton $B$ and $R0$ calculations in the same module and supplies the concrete integer required by the mass formula yardstick times phi to a rung offset.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.