cellTriangleCount_t11
plain-language theorem explainer
In one Kuhn-triangulated unit 4-cube there are exactly 72 oriented triangle hinges of difference-mask popcount type (1,1). Combinatorial gravity and Regge-calculus workers cite this when assembling per-orbit star kernels or checking that the six hinge types partition the 240 cell slots. The proof is a pure finite decision of the double sum that defines the cell count.
Claim. The cell-wide count of oriented triangle slots whose difference-mask popcount pair equals $(1,1)$ is $72$: summing the indicator of that type over the $24$ Kuhn simplices and the $10$ oriented index triples in each simplex yields $72$.
background
The module classifies triangle hinges in the Freudenthal/Kuhn triangulation of the unit 4-cube. Every oriented triangle in a Kuhn simplex is a monotone vertex-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 combinatorial 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 one cell. The cell-wide count for a fixed popcount pair $p$ is the double sum, over the $24$ simplices and the $10$ index triples per simplex, of the indicator that the triple has type $p$. The present statement evaluates that sum at $p=(1,1)$.
Scope is pure combinatorics of one unit cell up to lattice translation (difference masks) and triangulation-preserving symmetry; star kernels and the flat Hessian are out of scope here.
proof idea
The count is a concrete natural-number expression: a finite double sum of decidable Boolean indicators. The proof is the single tactic decide, which evaluates the sum by exhaustive computation over Fin 24 and Fin 10 and closes the equality to $72$. No intermediate lemmas are required beyond the definition of the cell count.
why it matters
This is the first entry in the per-type census $(72,48,48,24,24,24)$ for types $(1,1)$ through $(2,2)$. Downstream, cellTriangleCount_values packages all six equalities, and cellTriangleCount_sum uses them to prove the six types partition the $240$ oriented slots. In the Bloch-fold layer, the private lemma that counts type-$(1,1)$ hinges by an explicit indicator sum rewrites through this theorem to obtain $72$.
In the QG campaign the census is a combinatorial prerequisite for assembling the flat Hessian of the 4D Regge action from per-orbit star kernels. The seed hinge ${0,e_0,e_0+e_1}$ has type $(1,1)$, so this count anchors the principal orbit before $S_4$ and complement symmetries merge types into four lattice orbits. It does not itself evaluate kernels or close action-recovery gaps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.