pentEdgeVertices
plain-language theorem explainer
Canonical lexicographic enumeration of the ten edges of a 4-simplex on vertices {0,1,2,3,4}. Anyone working with CDT-style (4,1) or (3,2) simplices cites it to turn an edge index into an ordered vertex pair. The body is a pure pattern match, no proof.
Claim. The map $e \mapsto (i,j)$ sends each edge index $e \in \{0,\ldots,9\}$ to the ordered pair of endpoints among the five vertices of a 4-simplex, in lexicographic order: $(0,1),(0,2),(0,3),(0,4),(1,2),(1,3),(1,4),(2,3),(2,4),(3,4)$.
background
In 4D causal dynamical triangulations (Ambjørn–Jurkiewicz–Loll), spacetime between successive spatial slices is filled by 4-simplices of two combinatorial types: (4,1) with four vertices on slice $t$ and one on $t+1$, and (3,2) with a 3+2 split. Each 4-simplex has $\binom{5}{2}=10$ edges. Spacelike edges sit inside a single slice; timelike edges cross between slices.
This module fixes a global vertex set ${0,1,2,3,4}$ and a fixed ordering of those ten edges. The present definition is that ordering: edge index to endpoint pair. Downstream slice-membership and edge-type predicates read endpoints through this map, so the combinatorial tables for (4,1) and (3,2) stay synchronized with the geometry.
proof idea
No proof: a definition by exhaustive pattern match on Fin 10. Each constructor returns the corresponding ordered pair in lexicographic order. Downstream decide and fin_cases proofs simply unfold this table.
why it matters
Every causal-type and length-table lemma in the 4D CDT lane indexes edges through this map. The decide-able theorems isTimelike_fourOne_eq_crossSlice and isTimelike_threeTwo_eq_crossSlice verify that the hard-coded timelike edge sets equal the cross-slice pairs read off these endpoints. pentDistSq_edge shows the squared-distance table agrees with the edge tuple on every such pair. Outside the module, inducedSqEdges and shared_face_consistency in ThreePentCausalConsistency pull global lengths back along the same indexing, and realized in WickActionComplexFirst uses it for the Wick-rotated action. Without a single fixed edge order, the (4,1)/(3,2) edge-type counts, Cayley–Menger evaluations, and multi-chart consistency statements would not line up.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.