N0
plain-language theorem explainer
N0 defines the base cell count N₀(d) as twice the vertex count of the d-cube plus the single body cell. Researchers deriving fermion spans or the D=3 forcing condition in Recognition Science cite this when computing lepton and quark torsion numbers. The definition is a direct one-line combination of the sibling vertex function S0 and the constant cube_body.
Claim. $N_0(d) = 2V(d) + 1$, where $V(d)$ is the number of vertices of the $d$-dimensional hypercube.
background
The Sector-Dependent Generation Torsion module constructs integer cell counts for Q_D from binary-cube geometry. S0(d) equals the vertex count V(d) = 2^d. cube_body is the single D-cell and is fixed at 1. These enter the module's central claim that W = 2V + 1 holds only for d = 3, supplying a derived dimension-forcing condition independent of PDG data.
proof idea
One-line definition that applies the sibling definitions S0(d) := cube_vertices' d and cube_body := 1.
why it matters
N0 supplies the base count shown equal to the wallpaper number W at d = 3 in N0_eq_W_at_D3, which forces three spatial dimensions. It is used directly by lepton_span_eq_N0, down_span_plus_D_eq_W, N0_at_D3 and N1_minus_N0. The module doc states that this D = 3 coincidence is a genuine derivation; the assignment of specific counts to sectors remains a data-supported hypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.