sliceOf
plain-language theorem explainer
Assigns each of the five 4-simplex vertices to one of two adjacent CDT time slices. For type (4,1) only the apex sits on t+1; for type (3,2) the last two vertices do. Downstream decide-lemmas use it to certify that timelike edges are exactly the cross-slice pairs and to count vertices per slice. The body is a two-clause pattern match on the causal type.
Claim. Map each causal 4-simplex type and each vertex $v \in \{0,1,2,3,4\}$ to a Boolean slice tag: $\mathrm{false}$ means slice $t$, $\mathrm{true}$ means slice $t+1$. On type $(4,1)$ the tag is true exactly when $v=4$. On type $(3,2)$ it is true exactly when $v\in\{3,4\}$.
background
This module is the 4D Lorentzian lift of the CDT causal-simplex machinery (QG Seven-Gaps, Phase 3a). Between adjacent spatial slices one fills spacetime with two 4-simplex classes: type $(4,1)$ (four vertices on $t$, one on $t+1$) and type $(3,2)$ (three on $t$, two on $t+1$), with time reflections sharing the same edge-length data.
CausalPentType is the inductive label of those two classes. Vertices are indexed $0..4$; the ten edges run in lexicographic order. Spacelike edges carry squared length $a^2$; timelike edges carry $-\alpha a^2$ in the Lorentzian regime. Slice membership is the combinatorial input that later decides which edges are cross-slice (hence timelike).
The same pattern already appears in the 3D Wick module for tetrahedra; this definition is the 4D analogue used to ground edge-type tables and Cayley-Menger evaluations on both causal classes.
proof idea
Pure definition by cases on the causal type. On fourOne the Boolean is the equality test $v=4$. On threeTwo it is the disjunction $v=3\lor v=4$. No lemmas are invoked; the match is the entire content.
why it matters
Slice tags are the combinatorial backbone of the 4D CDT edge-type assignment. They feed the decide theorems isTimelike_fourOne_eq_crossSlice and isTimelike_threeTwo_eq_crossSlice, which prove an edge is timelike iff its endpoints lie on different slices, and the counting lemmas slice_count_fourOne / slice_count_threeTwo (4+1 and 3+2 vertex partitions). Parallel 3D uses appear in CausalSimplexWick for types $(3,1)$ and $(2,2)$.
Those facts lock the spacelike/timelike multiset before the Wick map $\alpha\mapsto -\alpha$ and the exact cm4 non-degeneracy thresholds. In the broader RS gravity lane this is kinematical scaffolding for the Lorentzian sector in $D=3$ spatial dimensions (forcing landmark T8), not a dynamical claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.