CausalTetType
plain-language theorem explainer
Enumerates the two causal tetrahedron classes of 3D CDT between adjacent spatial slices: (3,1) and (2,2). Anyone working the Lorentzian-sector lane of the QG Seven-Gaps campaign cites this as the discrete type index for edge assignments, Wick maps, and non-degeneracy thresholds. The declaration is a bare two-constructor inductive with no proof content.
Claim. There are exactly two causal tetrahedron types filling the spacetime between adjacent 2D spatial slices in 3D CDT: type $(3,1)$ (three vertices on slice $t$, one on $t+1$; time reflection $(1,3)$ shares the same edge data) and type $(2,2)$ (two vertices on each slice).
background
This module opens the first certified Lorentzian layer of the discrete gravity program. Prior formal and numerical results were Euclidean; here the setting is 3D Causal Dynamical Triangulations in the Ambjørn–Jurkiewicz–Loll convention.
Spatial slices are 2D triangulated surfaces of equilateral triangles with squared edge length $a^2$. Spacetime between slices $t$ and $t+1$ is filled by tetrahedra of two combinatorial types. Spacelike edges carry squared length $a^2$; timelike edges carry $-\alpha a^2$ in the Lorentzian regime ($\alpha>0$). Vertex indexing follows the Cayley–Menger polynomial convention: vertices $0,1,2,3$ and edges $0=(0,1),\ldots,5=(2,3)$.
Slice membership is fixed by type: for $(3,1)$, vertices ${0,1,2}$ lie on $t$ and $3$ on $t+1$; for $(2,2)$, ${0,1}$ on $t$ and ${2,3}$ on $t+1$. The time-reflected $(1,3)$ class is identified with $(3,1)$ at the level of edge-length multisets.
proof idea
No proof: this is a two-constructor inductive definition. The constructors name the two CDT tetrahedron classes; all subsequent combinatorial lemmas (slice membership, timelike/spacelike edge counts, squared-edge assignments) case-split on this type.
why it matters
This type is the discrete index for the entire Lorentzian-sector lane of the QG Seven-Gaps campaign. Downstream, non-degeneracy thresholds are defined by cases on it: $\alpha_{\min}(3,1)=1/3$ and $\alpha_{\min}(2,2)=1/2$, with positivity and $\alpha_{\min}<1$ proved by case analysis. Euclideanized Cayley–Menger positivity ($\mathrm{cm}3>0$) and the exact non-degeneracy range $\alpha>\alpha{\min}$ are likewise indexed by type.
The campaign ledger anchors proved flags against imported artifacts; this inductive sits under that Lorentzian stack. In the broader Recognition framework it supplies the $D=3$ causal simplex classes needed before Wick rotation ($\alpha\mapsto -\alpha$), deficit-angle reality at the physical point $\alpha=1$, and any later bridge from discrete Lorentzian geometry to continuum gravity claims.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.