cellTriangleCount_values
plain-language theorem explainer
In one Kuhn triangulation of the unit 4-cube, the six admissible popcount types of oriented triangle hinges occur with multiplicities 72, 48, 48, 24, 24, and 24. Anyone weighting lattice orbits when assembling the flat Hessian of the 4D Regge action from star kernels cites this census. The proof is a pure term packaging of six finite decide lemmas, one per type.
Claim. The cell-wide counts of oriented triangle slots of each admissible difference-mask popcount type equal $N(1,1)=72$, $N(1,2)=48$, $N(2,1)=48$, $N(1,3)=24$, $N(3,1)=24$, and $N(2,2)=24$, where $N(i,j)$ sums the indicator that a triangle in a Kuhn simplex has difference-mask type $(i,j)$ over all $24$ simplices and all $\binom{5}{3}=10$ oriented triples.
background
The module classifies triangle hinges in a single Freudenthal/Kuhn triangulation of the unit 4-cube. It is a combinatorial prerequisite for building the flat Hessian of the 4D Regge action from per-orbit star kernels. Scope is pure combinatorics of difference masks up to lattice translation and triangulation-preserving symmetry; kernels and Einstein-Hilbert recovery are out of scope.
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|)$ drawn from the six admissible pairs ${(1,1),(1,2),(2,1),(1,3),(3,1),(2,2)}$. There are exactly $24\cdot\binom{5}{3}=240$ oriented triangle slots in the cell.
The count $N(p)$ is the double sum, over the 24 Kuhn simplices and the 10 oriented triples, of the indicator that the triple has type $p$. The six individual equalities are already proved by finite decision; this theorem only packages them.
proof idea
Term-mode conjunction. The proof is the six-tuple of the already-proved equalities for types $(1,1)$, $(1,2)$, $(2,1)$, $(1,3)$, $(3,1)$, and $(2,2)$. Each of those lemmas is established by decide on the finite double sum that defines the cell-wide count. No algebraic reduction remains; the statement is literally the product of those six facts.
why it matters
Deliverable A of the Regge 4D hinge-orbit campaign requires the per-type census $(72,48,48,24,24,24)$ so that lattice orbits under $S_4$ (and under the larger group $S_4\rtimes{\mathrm{id},\mathrm{complement}}$) can be weighted correctly when assembling the flat Hessian from star kernels. The module doc lists this enumeration as item 2 of what is proved. Complement symmetry swaps type $(i,j)$ with $(j,i)$, merging the six types into four lattice orbits; these raw counts are the input to that merger.
No downstream Lean users are recorded yet. The module explicitly does not complete the flat Hessian, does not evaluate per-orbit star kernels beyond a committed seed, and does not flip gap-action recovery or prove $S_{\mathrm{RS}}\to\mathrm{EH}_{4d}$. The result is a closed combinatorial ledger for one Kuhn cell.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.