cellTriangleCount
plain-language theorem explainer
Defines the cell-wide tally of oriented triangle slots whose difference-mask popcount type equals a given pair p. Anyone assembling per-orbit hinge multiplicities in the 4D Kuhn cell cites it. The body is the double sum of the 0-1 type indicator over the 24 simplices and 10 triangle indices.
Claim. For a popcount pair $p\in\mathbb{N}\times\mathbb{N}$, let $N(p)$ be the number of oriented triangle slots $(s,t)$ in one unit 4-cube Kuhn triangulation with $s\in\{0,\ldots,23\}$ and $t\in\{0,\ldots,9\}$ such that the hinge difference-mask type of slot $(s,t)$ equals $p$. Explicitly $N(p)=\sum_{s}\sum_{t}\mathbf{1}_{\mathrm{type}(s,t)=p}$.
background
The module classifies triangle hinges in one unit 4-cube under the Freudenthal/Kuhn triangulation: 24 oriented 4-simplices, each carrying $C(5,3)=10$ oriented triangle faces, hence 240 oriented slots in total. Each such triangle is a monotone vertex-mask chain whose successive XOR differences $(a,b)$ are disjoint and nonzero; its combinatorial type is the popcount pair $(|a|,|b|)$, restricted to the six realizable values ${(1,1),(1,2),(2,1),(1,3),(3,1),(2,2)}$.
The upstream indicator triangleTypeNat returns 1 exactly when the hinge at simplex $s$ and local triangle index $t$ has popcount type $p$, and 0 otherwise. The present definition simply sums that indicator over the full cell. Scope is pure combinatorics of difference masks and lattice orbits; star kernels and the flat Hessian are out of scope here.
proof idea
Definition only: unfold as the double finite sum $\sum_{s:\mathrm{Fin},24}\sum_{t:\mathrm{Fin},10}$ of the 0-1 indicator that the hinge type of slot $(s,t)$ equals $p$. No tactics or lemmas beyond that sum of the sibling indicator.
why it matters
This is the raw multiplicity table that the orbit classification theorems evaluate. Downstream, the six concrete evaluations give the committed counts $(72,48,48,24,24,24)$ for types $(1,1)$ through $(2,2)$, and their sum theorem shows they partition all 240 slots. Hessian assembly equates abstract orbit cell counts to this function via orbitCellCount_eq_classification; Bloch-fold and all-orbit symbol lemmas rewrite oriented slot sums through it (e.g. the $(1,1)$ count equals 72). In the QG campaign it is the combinatorial prerequisite for folding per-orbit star kernels into the flat 4D Regge Hessian, without yet claiming Einstein-Hilbert recovery or gap-action closure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.