isTimelike_threeTwo_eq_crossSlice
plain-language theorem explainer
For a (3,2) causal 4-simplex in 4d CDT, an edge is timelike exactly when its two endpoints sit on different spatial slices. Anyone checking the Lorentzian edge-type table against the slice partition would cite this. The proof is a pure finite `decide` over the ten lexicographic edges.
Claim. For every edge $e$ among the ten edges of a 4-simplex of type $(3,2)$, the edge is timelike if and only if the two endpoints of $e$ lie on different spatial slices under the $(3,2)$ slice assignment.
background
This module is Phase 3a of the QG Seven-Gaps Lorentzian lane: the 4D CDT lift of the 3D causal-simplex machinery. Between adjacent spatial slices one fills spacetime with two 4-simplex types. Type $(3,2)$ places three vertices on slice $t$ and two on slice $t+1$, giving four spacelike edges and six timelike (cross-slice) edges; the time reflection $(2,3)$ shares the same edge-length multiset.
Edges of the 4-simplex on vertices ${0,1,2,3,4}$ are indexed lexicographically as a Fin 10. The map from edge index to endpoint pair is fixed once and for all. Slice membership is the combinatorial assignment of each vertex to $t$ or $t+1$ for the chosen type. Timelike means the edge joins the two slices; for $(3,2)$ that is the six cross edges with indices ${2,3,5,6,7,8}$.
The companion statement for type $(4,1)$ is the sibling cross-slice identity. Both feed the later Wick map and Cayley-Menger evaluations on the two causal classes.
proof idea
One-line decidability proof: decide. The domain is finite (ten edges, five vertices, two slices, Boolean equality), and both sides of the identity are closed Boolean expressions built from the explicit lookup tables for edge endpoints, slice assignment, and the hard-coded timelike mask for type $(3,2)$. Lean exhausts the cases; no algebraic lemma is required.
why it matters
The module builds the causal (CDT-style) 4-simplex classes in $D=4$ with spacelike/timelike edge types verified combinatorially from the slice structure. This lemma is the $(3,2)$ half of that verification: it pins the abstract timelike predicate to the geometric cross-slice condition, so later counts (six timelike, four spacelike) and the Wick continuation $\alpha\mapsto -\alpha$ rest on a machine-checked dictionary rather than a hand table.
It sits in the Lorentzian-sector lane of the Seven-Gaps campaign, parallel to the already kernel-checked 3D causal-simplex Wick module. No downstream theorem yet records a direct use, but the sibling slice-count and timelike-count lemmas in the same file are the natural consumers. Framework landmark: the $D=3$ spatial slices of the forcing chain appear here as the triangulated 3-manifolds that bound each 4-simplex.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.