slice_count_threeTwo
plain-language theorem explainer
Type (3,2) causal 4-simplices place three vertices on the earlier spatial slice and two on the later one. Anyone counting CDT edge types or setting up the 4D Wick map on squared lengths would cite this. The proof is a pure finite decision on the Boolean slice assignment for Fin 5.
Claim. For the causal 4-simplex type $(3,2)$, the five vertices split as three on slice $t$ and two on slice $t+1$: $|\{v:\mathrm{slice}(v)=t\}|=3$ and $|\{v:\mathrm{slice}(v)=t+1\}|=2$.
background
This module is the 4D Lorentzian lift of the kernel-checked 3D causal-simplex machinery (Ambjørn–Jurkiewicz–Loll CDT conventions). Between adjacent spatial slices of equilateral tetrahedra, spacetime is filled by two 4-simplex classes: type (4,1) with four vertices on slice $t$ and one on $t+1$, and type (3,2) with three on $t$ and two on $t+1$ (reflections (1,4) and (2,3) share the same edge-length multisets).
CausalPentType is the inductive label of those two classes. The local map sliceOf assigns each vertex in Fin 5 a Boolean slice tag: for type (3,2), vertices $0,1,2$ sit on slice $t$ (false) and vertices $3,4$ on slice $t+1$ (true). Spacelike edges stay inside a slice; timelike edges cross slices and later carry squared length $-\alpha a^2$ in the Lorentzian regime.
The 3D precursor in CausalSimplexWick uses the same slice-tag pattern on tetrahedra ((3,1) and (2,2)). The present lemma is the 4D counting counterpart for the (3,2) class.
proof idea
One-line decide proof. The domain is Fin 5 with a closed-form Boolean sliceOf for CausalPentType.threeTwo, so both filtered cardinalities are finite decidable equalities; Lean evaluates them by exhaustive computation and closes the conjunction.
why it matters
In the QG Seven-Gaps Lorentzian-sector lane (Phase 3a), combinatorial slice counts are the first gate before edge-type assignment, squared-length vectors, and the Cayley–Menger evaluation cm4. This lemma locks the (3,2) vertex split that the module docstring quotes as "3 + 1 = 4 spacelike + 6 timelike edges," so later decide-lemmas on timelike/spacelike edge counts and the Wick involution alpha ↦ -alpha rest on a fixed partition rather than an ad-hoc labeling.
No downstream theorems currently depend on it in the graph, but sibling counts (slice_count_fourOne, timelike_count_threeTwo, etc.) form the same decide-layer that feeds non-degeneracy thresholds for both causal classes. Framework-wise it sits under the D = 3 spatial-slice convention of T8, lifted one dimension for CDT 4-simplices; it does not itself touch the forcing chain or the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.