subcellCount_vertex
plain-language theorem explainer
The 3-cube has exactly eight vertices: subcell count at CW-dimension 0 equals 8 when spatial dimension is D=3. Anyone citing the CW-filtration schedule for generation torsion (vertices before edges before faces) needs this base count. The proof is a one-line native evaluation of the closed-form vertex formula at D=3.
Claim. With spatial dimension $D=3$, the number of $0$-cells (vertices) of the $D$-cube equals $8$. Equivalently, $\mathrm{subcell\,count}(D,\mathrm{vertex})=2^D=8$.
background
The module builds excitation ordering for fermion generation torsion from the CW-filtration of the spatial 3-cube $Q_3$. The 0-skeleton is the vertex set; the 1-skeleton adds edges; the 2-skeleton adds faces. Generation excitations are assumed to couple in increasing CW dimension, producing the cumulative torsion schedule ${0,11,17}$.
Spatial dimension is fixed at $D=3$ by the forcing chain (T8). The local helper subcellCount dispatches on cell type: vertices map to the hypercube vertex count $2^d$, edges to the edge count, faces to the face count. This theorem pins the vertex case at the forced $D$.
Upstream, $D$ is defined as the constant $3$ in the alpha, gap, and fermion-DOF bridges; the eight-tick octave $2^3$ is the same combinatorial factor that appears here as the vertex count of $Q_3$.
proof idea
One-line proof by native_decide. Unfolding the definition, the vertex branch is the closed form $2^D$; substituting the constant $D=3$ yields $8$, which the kernel decides by computation. No lemmas are invoked beyond definitional reduction.
why it matters
This is the base rung of the CW-filtration arithmetic that the module uses to replace ad-hoc mode labels (ground/edge/face) in cube-admissible torsion with a single geometric principle. Gen 1 couples only to the 0-skeleton, so torsion starts at $\tau=0$ precisely because there are eight vertices and no higher cells yet engaged.
It sits under the module claim that IF excitations couple in CW-dimension order, THEN the first nontrivial excitation is edge-supported and the torsion schedule matches the canonical ${0,11,17}$, with J-cost strictly ordered $J(\varphi^0)<J(\varphi^{11})<J(\varphi^{17})$. The vertex count $8=2^3$ is also the combinatorial shadow of the eight-tick octave forced at T7 and of $D=3$ at T8.
No downstream theorems currently depend on this simp fact in the graph; it is local scaffolding for the sibling edge/face count lemmas and the passive-coupling positivity facts in the same file. The remaining open premise is the filtration principle itself (coupling order), not this count.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.