subcellCount_face
plain-language theorem explainer
The 3-cube has exactly six 2-faces. Anyone building the CW-filtration torsion schedule for fermion generations cites this as the face contribution. The proof is a one-line native decision of the closed combinatorial count at D=3.
Claim. For spatial dimension $D=3$, the number of face-type subcells of the $D$-cube equals $6$: $\mathrm{subcellCount}(D,\mathrm{face})=6$.
background
The module treats generation excitations as coupling to the CW-filtration of the spatial 3-cube $Q_3$. The 0-skeleton has 8 vertices, the 1-skeleton 12 edges (11 passive), and the 2-skeleton 6 faces. Cumulative torsion then reads ${0,11,17}$ once excitations attach in dimension order.
subcellCount is the pure combinatorial counter: on a $d$-cube it returns vertex, edge, or face cardinality according to the cell label. Spatial dimension $D$ is the constant $3$ forced by the T8 step of the forcing chain (and re-exported from several bridges).
The face case is the last rung of that count: six 2-cells complete the filtration used for the third-generation torsion increment.
proof idea
One-line native_decide proof. After unfolding subcellCount at the face constructor and substituting $D=3$, the goal reduces to the closed formula for the number of 2-faces of the 3-cube, which the kernel evaluates to 6.
why it matters
In the excitation-ordering argument, Gen 3 attaches the 2-skeleton and adds the face count to the passive-edge torsion: $\tau=11+6=17$. This lemma discharges that arithmetic step and supplies the `@[simp]$ normal form used by the later passive-coupling and J-cost comparisons $J(\varphi^0)<J(\varphi^{11})<J(\varphi^{17})$.
It sits inside the structural explanation of why edges precede faces in CubeAdmissibleTorsion: the ordering is the CW-dimension order on $Q_3$, not an extra mode label. The remaining open premise is the filtration principle itself (excitations couple in CW-dimension order), which this count does not address. Landmark link: $D=3$ from T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.