isTimelike
plain-language theorem explainer
Boolean edge classifier for the two CDT 4-simplex types: marks which of the ten lexicographic edges are timelike (cross-slice). For (4,1) the four apex-touching edges; for (3,2) the six bipartition cross edges. Downstream Euclidean/Lorentzian squared-length maps and Wick continuation branch on it. Pure pattern-match table, no proof obligations.
Claim. Define a Boolean predicate on causal 4-simplex type and edge index $e \in \{0,\ldots,9\}$: for type $(4,1)$, return true precisely when $e \in \{3,6,8,9\}$; for type $(3,2)$, return true precisely when $e \in \{2,3,5,6,7,8\}$. True means the edge is timelike (joins the two spatial slices).
background
In 4d causal dynamical triangulations (Ambjørn–Jurkiewicz–Loll), spacetime between adjacent spatial slices is filled by two 4-simplex classes. Type $(4,1)$ places four vertices on slice $t$ and one apex on $t+1$ (six spacelike, four timelike edges). Type $(3,2)$ places three on $t$ and two on $t+1$ (four spacelike, six timelike). Time reflections $(1,4)$ and $(2,3)$ share the same edge-length multisets.
Vertices are labeled $0..4$; the ten edges run in lexicographic order $(0,1),(0,2),\ldots,(3,4)$. Spacelike edges carry squared length $a^2$; timelike edges carry $-\alpha a^2$ in the Lorentzian regime ($\alpha>0$). The Wick map flips the sign of the timelike squared lengths, equivalently $\alpha\mapsto -\alpha$.
This definition is the combinatorial edge-type table used by every subsequent squared-length assignment in the module. Companion decide-lemmas check it against the slice partition: an edge is marked timelike iff its two endpoints (via the edge-to-vertex map) lie on different slices.
proof idea
No proof body: a definition by cases on the inductive causal type. Each branch is a Boolean disjunction on the raw Fin 10 value, hard-coding the standard CDT edge tables. Correctness relative to slice structure is discharged later by two decide theorems that equate this table to the cross-slice predicate built from the vertex-pair map and the slice assignment.
why it matters
Phase 3a of the QG Seven-Gaps Lorentzian lane: the 4d lift of the kernel-checked 3d causal-simplex Wick machinery. Every Euclideanized and Lorentzian squared-edge tuple branches on this predicate (spacelike $\mapsto a^2$, timelike $\mapsto \pm\alpha a^2$), so positivity, scaling, regular-simplex specialization at $\alpha=1$, and the Wick involution all depend on it.
The two decide-lemmas that follow pin the table to the slice bipartition, closing the combinatorial side of the edge-type assignment before Cayley–Menger evaluation and non-degeneracy thresholds in $\alpha$. In the broader Recognition gravity stack this is pure CDT kinematics (D=4 forced elsewhere by T8); it supplies the discrete Lorentzian class on which continuum limits and Regge-type actions sit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.