subcellCount
plain-language theorem explainer
Maps each subcell type of the D-cube (vertex, edge, face) to its combinatorial count: 2^D vertices, D·2^(D-1) edges, and 2D faces. Mass and generation-torsion arguments cite it when building the CW-filtration schedule on Q_3. The body is a three-clause pattern match onto the standard hypercube counting formulas.
Claim. For each dimension $D\in\mathbb{N}$ and each subcell type $c$ of the $D$-cube $Q_D$ (vertex, edge, or face), the total number of such subcells is $2^D$ if $c$ is a vertex, $D\cdot 2^{D-1}$ if $c$ is an edge, and $2D$ if $c$ is a face.
background
The module derives edge-before-face excitation ordering for fermion generation torsion from the CW-complex of the $D=3$ cube $Q_3$, together with $J$-cost monotonicity on $\varphi$-power ratios. Subcell types are restricted to the three grades relevant for generation coupling: vertices (CW-dim 0), edges (CW-dim 1), and faces (CW-dim 2).
Standard hypercube counts supply the numerics. Vertices of $Q_D$ number $2^D$; edges number $D\cdot 2^{D-1}$; faces number $2D$. For $D=3$ these specialize to 8, 12, and 6, matching the module's skeleton description (8 vertices; 12 edges of which 11 are passive; 6 faces).
Those counts feed the cumulative torsion schedule ${0,11,17}$: ground couples only to the 0-skeleton ($\tau=0$), the first excitation adds 1-cells ($\tau=11$), and the second adds 2-cells ($\tau=11+6=17$).
proof idea
Definition by cases on the inductive subcell type. Vertex maps to the hypercube vertex count $2^D$, edge to $D\cdot 2^{D-1}$, and face to $2D$. No proof obligations; the three arms are pure abbreviations of the upstream counting defs.
why it matters
Gives a single typed interface for the three skeleton sizes that drive the CW-filtration argument in this module. Downstream simp lemmas pin the $D=3$ values (8 vertices, 12 edges, 6 faces), which are the concrete inputs to the torsion schedule ${0,11,17}$ and to the strict $J$-cost chain $J(\varphi^0)=0<J(\varphi^{11})<J(\varphi^{17})$.
In the broader Recognition chain this sits under $T8$ ($D=3$ spatial dimensions) and the eight-tick octave ($2^3=8$ vertices). It replaces ad-hoc mode labels in cube-admissible torsion with geometric cell counts, so the remaining premise is only that excitations couple in CW-dimension order.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.