cellTriangleCount_sum
plain-language theorem explainer
The six admissible popcount types of difference-mask pairs for oriented triangles in one Kuhn 4-cell sum to exactly 240 slots. Combinatorial gravity workers assembling the 4D Regge flat Hessian cite this as the partition check that every oriented triangle is typed. Proof is a one-line simplification of the six per-type enumeration theorems (72+48+48+24+24+24).
Claim. The sum of the cell-wide oriented-triangle counts over the six admissible popcount types $(1,1)$, $(1,2)$, $(2,1)$, $(1,3)$, $(3,1)$, and $(2,2)$ equals $240$.
background
In the Freudenthal/Kuhn triangulation of the unit 4-cube there are 24 simplices, and each contributes $\binom{5}{3}=10$ oriented triangle faces, hence $24\cdot 10=240$ oriented triangle slots in one cell. Every index-triple triangle is a monotone vertex-mask chain $m_0\subset m_1\subset m_2$ whose successive difference masks $(a,b)=(m_1\oplus m_0,m_2\oplus m_1)$ are disjoint and nonzero; its type is the popcount pair $(|a|,|b|)$, forced into exactly ${(1,1),(1,2),(2,1),(1,3),(3,1),(2,2)}$.
The cell-wide count for a fixed type is the double sum, over the 24 simplices and 10 triangle indices, of the indicator that the triangle has that type. Sibling theorems already fix the six counts at $72,48,48,24,24,24$ respectively (each by finite decision). This module supplies the combinatorial prerequisite for assembling the flat Hessian of the 4D Regge action from per-orbit star kernels; it never redefines the 24-simplex or vertex-mask APIs it imports.
proof idea
One-line term proof. simp rewrites each of the six summands by the corresponding per-type count theorem (the six results that fix the counts at $72$, $48$, $48$, $24$, $24$, and $24$). The goal collapses to the arithmetic identity $72+48+48+24+24+24=240$, which closes under the same simplification. No case split or induction is required; the work sits entirely in the upstream finite enumerations.
why it matters
This is deliverable A item 2 of the Regge 4D triangle-hinge orbit classification: the six types partition all $240$ oriented slots, with explicit multiplicities $(72,48,48,24,24,24)$. It closes the cell-enumeration half of the combinatorial prerequisite for the QG full-theory campaign's flat-Hessian assembly from per-orbit star kernels. Any later multiplicity bookkeeping or normalization of star-kernel contributions against the full cell will rest on this identity; no formal dependents are recorded yet in the graph. The result is pure combinatorics inside one unit 4-cube and does not touch the forcing chain T0-T8, the Recognition Composition Law, continuum recovery of Einstein-Hilbert, or the gap-action flag.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.