cellTriangleCount_t31
plain-language theorem explainer
In one Kuhn-triangulated 4-cube there are exactly 24 oriented triangle hinges of difference-mask type (3,1). Combinatorial gravity and Regge-calculus workers cite this when assembling the flat Hessian from per-orbit star kernels. The equality is discharged by decidable evaluation of the double sum that defines the cell-wide type count.
Claim. The number of oriented triangle slots in one unit 4-cube Kuhn cell whose difference-mask popcount type is $(3,1)$ equals $24$.
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. Scope is pure combinatorics: lattice translation (difference masks) and triangulation-preserving symmetry; no star kernels or continuum limits are evaluated here.
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 $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 per simplex of the indicator that the triple has type $p$. Type $(3,1)$ is one of the six realizable classes; complement symmetry swaps it with $(1,3)$.
proof idea
One-line decidable proof: decide evaluates the finite double sum defining the cell-wide count at $p=(3,1)$ and checks equality with 24. No intermediate lemmas are invoked beyond the definition of the count itself.
why it matters
This is one of the six explicit per-type evaluations that feed cellTriangleCount_values (the bundled statement of all six counts $(72,48,48,24,24,24)$) and cellTriangleCount_sum (the partition identity that the six types exhaust all 240 oriented slots). Together they discharge deliverable A.2 of the module: cell enumeration of triangle hinges by difference-mask type.
In the QG full-theory campaign these counts fix orbit multiplicities before star kernels are assembled into the flat Hessian. The module explicitly does not yet evaluate per-orbit kernels (beyond a committed seed), complete the flat Hessian, prove $S_{\mathrm{RS}}$ converges to Einstein–Hilbert in 4D, or flip gap_action_recovery. The $(3,1)$ count is the complement twin of $(1,3)$; under $S_4\rtimes{\mathrm{id},\mathrm{complement}}$ the two merge into one lattice orbit among the four coarse orbits.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.