isTimelike_fourOne_eq_crossSlice
plain-language theorem explainer
For a causal 4-simplex of type (4,1), an edge is timelike exactly when its two endpoints sit on different spatial slices. Anyone checking the CDT edge-type table against the slice partition cites this. The proof is a pure `decide` over the ten edges and five vertices.
Claim. For every edge index $e \in \{0,\ldots,9\}$ of a type-$(4,1)$ causal 4-simplex, the edge is timelike if and only if the two endpoints of $e$ lie on different slices (one on slice $t$, one on slice $t+1$).
background
This module is the 4D Lorentzian lift of the 3D causal-simplex machinery, in the QG Seven-Gaps Lorentzian-sector lane. In 4d CDT (Ambjørn–Jurkiewicz–Loll), spacetime between adjacent spatial slices is filled by two 4-simplex types. Type (4,1) places four vertices on slice $t$ and one apex on slice $t+1$; its edge multiset is six spacelike plus four timelike.
Vertices are indexed by $\mathrm{Fin},5$; the ten edges run in lexicographic order $(0,1),\ldots,(3,4)$. Slice membership sends vertices $0,1,2,3$ to slice $t$ and vertex $4$ to $t+1$. The edge-type predicate marks an edge timelike precisely when it is one of ${3,6,8,9}$ (the four edges that touch the apex). The claim equates that combinatorial table with the geometric cross-slice condition.
proof idea
One-line decide proof. Both sides are Boolean functions of a finite domain (Fin 10 edges, with vertex pairs and slice tags also finite and definitionally closed). Lean exhausts the ten cases and checks equality of the two Bool expressions on each. No algebraic lemmas are invoked beyond the decidable equality infrastructure.
why it matters
Phase 3a of the Seven-Gaps campaign needs the spacelike/timelike assignment verified combinatorially from the slice structure before Wick rotation, Cayley–Menger evaluation, and non-degeneracy thresholds can be stated. This lemma (and its (3,2) twin) discharges that table-check for type (4,1): timelike means cross-slice, nothing more. Downstream material in the same module (Wick map as $\alpha\mapsto -\alpha$, exact cm4 on both classes, Euclidean thresholds) relies on this identification being definitionally locked. It sits in the Lorentzian sector that ultimately feeds the $D=3$ spatial forcing (T8) and the eight-tick causal scaffolding, though this declaration itself is pure 4-simplex combinatorics. No used_by edges are recorded yet; the immediate consumers are the sibling count lemmas and the Wick/cm4 development in-module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.