cellTriangleCount_t13
plain-language theorem explainer
In one Kuhn-triangulated unit 4-cube there are exactly 24 oriented triangle hinges of difference-mask type (1,3). Combinatorialists assembling the flat Regge Hessian from per-orbit star kernels cite this count. The proof is a pure `decide` discharge of a finite double sum over the 24 simplices and 10 index triples.
Claim. The number of oriented triangle slots in one Kuhn cell whose difference-mask popcount type is $(1,3)$ 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 combinatorics only: lattice translation (difference masks) and triangulation-preserving symmetry; no star-kernel evaluation and no claim that the RS action converges to Einstein–Hilbert.
Every index-triple triangle inside 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 counter cellTriangleCount sums, over the 24 Kuhn simplices and the 10 oriented triples per simplex, the indicator that the triple has a prescribed popcount type. The present theorem evaluates that counter at type $(1,3)$.
proof idea
One-line decidability proof. Unfolding the definition yields a finite double sum of Boolean indicators over Fin 24 and Fin 10; Lean’s decide tactic evaluates the closed natural-number expression and closes the equality to 24.
why it matters
This is one of the six atomic per-type counts that feed the cell enumeration deliverable of the module. Downstream, cellTriangleCount_values packages the six equalities (including this one) as a single conjunction, and cellTriangleCount_sum uses them to prove the types partition all 240 oriented slots: $72+48+48+24+24+24=240$.
Those counts are the combinatorial skeleton for orbit classification under $S_4$ and under the larger group $S_4\rtimes{\mathrm{id},\mathrm{complement}}$, which merges $(1,3)$ with $(3,1)$ into one of four lattice orbits. The module is explicit that this does not yet evaluate per-orbit star kernels, complete the flat Hessian, prove $S_{\mathrm{RS}}$ converges to EH in 4D, or flip gap_action_recovery. It is a proved brick in the QG full-theory campaign’s combinatorial layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.