cellTriangleCount_t12
plain-language theorem explainer
In one unit 4-cube Kuhn triangulation there are exactly 48 oriented triangle hinges of difference-mask popcount type (1,2). Combinatorial gravity and Regge-calculus workers cite this as one of the six per-type cell counts. The proof is a pure finite decision: the double sum over 24 simplices and 10 index triples is evaluated by decidability.
Claim. In the Freudenthal/Kuhn triangulation of the unit 4-cube, the number of oriented triangle slots whose difference-mask popcount pair equals $(1,2)$ is exactly $48$.
background
The module classifies triangle hinges in one unit 4-cube under the Kuhn (Freudenthal) triangulation: 24 simplices, each contributing $C(5,3)=10$ oriented index-triple triangles, for 240 oriented slots in total. Each such triangle 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)}$.
The cell-wide counter sums, over all 24 simplices and all 10 triples per simplex, the indicator that the triple has a prescribed popcount type. The present statement fixes that type to $(1,2)$. Scope is pure combinatorics of difference masks up to lattice translation; no curvature weights or star kernels are evaluated here.
proof idea
One-line decide proof. The counter is a finite double sum of a decidable Boolean predicate (triangle type equals the pair $(1,2)$) over Fin 24 and Fin 10, so Lean reduces the equality to $48$ by exhaustive evaluation of a decidable proposition. No algebraic lemmas beyond the definition of the counter are required.
why it matters
This is one of the six explicit per-type counts that make the cell enumeration concrete: the module claims the oriented tally vector $(72,48,48,24,24,24)$ for types $(1,1),(1,2),(2,1),(1,3),(3,1),(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 Recognition Science gravity campaign this is deliverable A of the Regge 4D hinge-orbit classification: a combinatorial prerequisite for assembling the flat Hessian from per-orbit star kernels. It does not itself evaluate kernels, complete the flat Hessian, or prove continuum recovery of the Einstein-Hilbert action; those remain separate campaign steps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.