cellTriangleCount_t22
plain-language theorem explainer
Oriented triangle slots of difference-mask popcount type (2,2) in one Kuhn 4-cell number exactly 24. Regge/QG analysts cite this when tallying the six hinge types that partition the 240 oriented slots of a Freudenthal cell. The proof is a one-line decidability check on the finite double sum that defines the cell-wide count.
Claim. In one unit 4-cube Kuhn cell, the number of oriented triangle slots whose disjoint difference-mask popcounts equal $(2,2)$ is exactly $24$.
background
This module classifies triangle hinges in the Freudenthal/Kuhn triangulation of the unit 4-cube. 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$ Kuhn simplices and $C(5,3)=10$ oriented triples per simplex, hence $240$ oriented triangle slots per cell. The cell-wide count of a given popcount type is the double sum, over the $24$ simplices and $10$ triples, of the indicator that the triple has that type.
The local setting is combinatorics only: lattice translation (difference masks) and triangulation-preserving symmetry. No star kernels or Hessian entries are evaluated here.
proof idea
One-line decidability proof. The cell count is a finite double sum of a decidable Nat-valued indicator over Fin 24 and Fin 10, so decide evaluates the sum at the pair $(2,2)$ and closes the equality to $24$.
why it matters
Fills one of the six per-type count identities that constitute deliverable A of the Regge 4D hinge-orbit campaign: the oriented counts $(72,48,48,24,24,24)$ for types $(1,1)$ through $(2,2)$. Downstream, cellTriangleCount_values packages all six equalities as a single conjunction, and cellTriangleCount_sum uses them to prove the types partition the $240$ slots.
Those tallies are the combinatorial prerequisite for assembling the flat Hessian of the 4D Regge action from per-orbit star kernels. The module explicitly does not yet evaluate those kernels (beyond a committed seed), complete the flat Hessian, prove $S_{RS}$ converges to Einstein-Hilbert in 4D, or flip the action-recovery gap flag. This lemma is pure bookkeeping that makes the later orbit assembly honest.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.