cellTriangleCount_t21
plain-language theorem explainer
In one Kuhn-triangulated unit 4-cube there are exactly 48 oriented triangle hinges of difference-mask popcount type (2,1). Combinatorial gravity and Regge-calculus workers cite this when assembling the flat Hessian from per-orbit star kernels. The equality is discharged by a single decidability check on the finite double sum that defines the cell-wide count.
Claim. The number of oriented triangle slots in one Kuhn cell whose difference-mask popcount type is $(2,1)$ equals $48$.
background
The module classifies triangle hinges in the Freudenthal/Kuhn triangulation of the unit 4-cube, a combinatorial prerequisite for building the flat Hessian of the 4D Regge action from per-orbit star kernels. It works only with combinatorics of one cell, up to lattice translation (difference masks) and triangulation-preserving symmetry.
Every index-triple triangle in a Kuhn simplex is a monotone mask chain $m_0 \subset m_1 \subset m_2$ with disjoint nonzero difference masks $(a,b)=(m_1\oplus m_0,m_2\oplus m_1)$. Its type is the popcount pair $(|a|,|b|)$ in ${(1,1),(1,2),(2,1),(1,3),(3,1),(2,2)}$. There are exactly $24\cdot C(5,3)=240$ oriented triangle slots in the cell.
The cell-wide count cellTriangleCount of a given popcount type $p$ is the double sum, over the 24 Kuhn simplices and the 10 oriented triples in each, of the indicator that the triple has type $p$.
proof idea
One-line decidability proof. The definition of the cell-wide count is a finite sum of natural-number indicators over Fin 24 and Fin 10, so the equality to 48 is a closed decidable statement and is closed by decide.
why it matters
This is one of the six explicit per-type counts that make deliverable A of the module concrete: oriented slot counts $(72,48,48,24,24,24)$ for types $(1,1),(1,2),(2,1),(1,3),(3,1),(2,2)$. Downstream, cellTriangleCount_values packages all six equalities, and cellTriangleCount_sum shows they partition the 240 oriented slots.
In the QG full-theory campaign these counts feed the lattice-orbit classification under coordinate permutation and complement symmetry (four orbits after merging $(i,j)$ with $(j,i)$). They do not yet evaluate star kernels or close the flat Hessian; they only fix the combinatorial multiplicities needed before those analytic steps. Framework-wise this sits in the gravity/Regge side of Recognition Science, not in the T0–T8 forcing chain itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.