sliceOf
plain-language theorem explainer
Assigns each tetrahedron vertex to one of two adjacent CDT time slices. For type (3,1) only the apex sits on t+1; for (2,2) the last two vertices do. Gravity and CDT workers cite it as the combinatorial source of spacelike vs timelike edges. The body is a two-clause pattern match on CausalTetType.
Claim. For each causal tetrahedron type $\tau\in\{(3,1),(2,2)\}$ and each vertex $v\in\{0,1,2,3\}$, return a Boolean slice label: $\mathrm{false}$ means slice $t$, $\mathrm{true}$ means slice $t+1$. On type $(3,1)$ the label is true exactly when $v=3$; on type $(2,2)$ it is true exactly when $v\in\{2,3\}$.
background
This module opens the Lorentzian sector of the QG Seven-Gaps campaign in $D=3$ CDT (Ambjørn–Jurkiewicz–Loll). Spatial slices are 2D equilateral triangulations with squared edge length $a^2$; the slab between $t$ and $t+1$ is filled by two tetrahedron classes: type $(3,1)$ (three vertices on $t$, one on $t+1$) and type $(2,2)$ (two on each slice). Spacelike edges keep $a^2$; timelike edges carry $-\alpha a^2$ with $\alpha>0$.
Vertex indexing follows the Cayley–Menger convention: vertices $0,1,2,3$ and edges $0=(0,1),,1=(0,2),,2=(0,3),,3=(1,2),,4=(1,3),,5=(2,3)$. The inductive type CausalTetType names the two classes. Slice membership is the Boolean predicate that later decides which edges cross the cut and are therefore timelike.
proof idea
Pure definition by pattern match: no proof obligations. On threeOne the predicate is the equality test $v=3$; on twoTwo it is the disjunction $v=2\lor v=3$. Both branches are decidable Boolean expressions on Fin 4.
why it matters
Slice membership is the combinatorial root of the whole Lorentzian edge-type table. Downstream, isTimelike_threeOne_eq_crossSlice and isTimelike_twoTwo_eq_crossSlice prove by decide that an edge is timelike exactly when its endpoints receive opposite slice labels; the companion slice_count_* lemmas certify the expected $(3,1)$ and $(2,2)$ partition cardinalities. The same pattern is lifted to 4D pentachora in CausalSimplex4D.sliceOf. Together these facts underwrite the Wick map $\alpha\mapsto -\alpha$ on squared lengths and the deficit-angle reality corollary at the physical point $\alpha=1$, closing the first certified Lorentzian layer of the discrete gravity program (T8 forces $D=3$ spatial dimensions, matching the 3D CDT setting).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.