triangleIndexTriple
plain-language theorem explainer
Enumerates the ten increasing triples of vertex indices among the five vertices of a 4-simplex: the standard C(5,3) listing. Anyone assembling triangle hinges inside a Kuhn 4-simplex cites this table. The body is a pure pattern-match lookup with an absurd branch for out-of-range Fin 10.
Claim. A fixed enumeration of all strictly increasing triples $(i,j,k)$ with $0 \le i < j < k \le 4$, indexed by $\{0,\ldots,9\}$. Equivalently, the map sending each of the $\binom{5}{3}=10$ unordered 3-subsets of the five vertices of a 4-simplex to its unique increasing ordered triple.
background
The ambient module classifies triangle hinges in the Freudenthal/Kuhn triangulation of the unit 4-cube. A 4-simplex has five vertices; each triangle face is a 3-subset of those vertices. There are exactly $\binom{5}{3}=10$ such faces, so triangle slots inside one simplex are indexed by $\mathrm{Fin},10$.
The module imports the 24 Kuhn simplices and the vertexMask API from the flat-kernel analysis, together with the 15-class edge-mask utilities. It never redefines those; it only builds the combinatorial orbit layer on top. Difference masks and popcount types (pairs in ${(1,1),(1,2),(2,1),(1,3),(3,1),(2,2)}$) are computed from ordered triples of vertex masks, so a canonical listing of the ten index triples is the first bookkeeping step.
Scope is combinatorics only: lattice translation (difference masks) and triangulation-preserving symmetry inside one unit 4-cube. No star kernels, no flat Hessian, and no continuum Einstein-Hilbert recovery are claimed here.
proof idea
Definition by exhaustive pattern match. Cases $0$ through $9$ list the ten increasing triples $(0,1,2),\ldots,(2,3,4)$ in lexicographic order. The residual Fin constructor $\langle n+10,h\rangle$ is discharged by absurd plus omega, since no inhabitant of $\mathrm{Fin},10$ has value $\ge 10$. No lemmas are invoked.
why it matters
This table is the shared index of triangle slots used throughout the 4D Regge hinge campaign. Downstream, triangleVertexMasks reads the triple and looks up the three vertex masks of simplex $s$, which then feed difference masks, popcount orbit types, and the six-type (later four-orbit) classification. The Schlaefli pathwise module aliases the same map as its local hinge index, so every pathwise hinge identity inherits this enumeration.
In the QG full-theory stack this is deliverable-A bookkeeping: without a fixed $C(5,3)$ listing one cannot count the $24\cdot 10=240$ oriented triangle slots or prove the per-type multiplicities $(72,48,48,24,24,24)$. It does not itself close gap-action recovery or $S_{\mathrm{RS}}\to\mathrm{EH}_{4d}$; it only makes the orbit census well-defined.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.