CausalPentType
plain-language theorem explainer
Enumerates the two CDT causal 4-simplex classes between adjacent spatial slices: (4,1) and (3,2). Anyone working the 4D Lorentzian lift, Wick map, or Cayley–Menger thresholds cites this as the type index. It is a bare two-constructor inductive with no proof content.
Claim. There are exactly two causal 4-simplex types in 4D CDT between adjacent slices: type $(4,1)$ (four vertices on slice $t$, one on $t+1$; time reflection $(1,4)$ shares the same edge data) and type $(3,2)$ (three on $t$, two on $t+1$; reflection $(2,3)$ likewise).
background
This module is Phase 3a of the QG Seven-Gaps Lorentzian-sector lane: the 4D CDT lift of the 3D causal-simplex Wick machinery. Spatial slices are equilateral 3-manifolds with squared edge length $a^2$. Spacetime between slices $t$ and $t+1$ is filled by two 4-simplex classes in the Ambjørn–Jurkiewicz–Loll convention.
Type $(4,1)$ has six spacelike and four timelike edges; type $(3,2)$ has four spacelike and six timelike edges. Spacelike squared lengths are $a^2$; timelike ones are $-\alpha a^2$ in the Lorentzian regime ($\alpha>0$). The ten edges of a 4-simplex are indexed lexicographically on vertices $0..4$.
The sole upstream dependency is a trivial edge complex from the Gap-2 gluing derivation (two vertices, one edge). It does not constrain the causal classification; the type is pure combinatorial bookkeeping for later edge-length and Cayley–Menger maps.
proof idea
No proof: a two-constructor inductive definition. The constructors fourOne and threeTwo name the $(4,1)$ and $(3,2)$ CDT classes. Downstream definitions and theorems case-split on this type (typically cases ty) to assign edge patterns, Wick images, and exact $\alpha$ thresholds.
why it matters
This is the discrete type index for the entire 4D causal-simplex stack. Downstream, alphaMin assigns the exact Euclidean non-degeneracy thresholds ($3/8$ for $(4,1)$, $7/12$ for $(3,2)$); positivity, degeneracy-at-threshold, and Lorentzian negativity theorems for the bordered Cayley–Menger determinant cm4 all case on it. Slice and timelike/spacelike edge counts, and the Wick involution acting as $\alpha\mapsto -\alpha$, are likewise typed by it.
In the Recognition gravity program this closes the combinatorial half of the 4D kinematical Wick rotation (T8 forces $D=3$ spatial dimensions, hence 4-simplices in spacetime). Without a finite causal-type enum, the exact $\mathrm{cm}_4$ thresholds and the Euclidean/Lorentzian sign flip cannot be stated uniformly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.