slice_count_twoTwo
plain-language theorem explainer
Type (2,2) causal tetrahedra in 3D CDT place exactly two of four vertices on each adjacent spatial slice. Anyone building the Lorentzian CDT layer, edge-type assignments, or the Wick map would cite this count. The proof is a one-line finite decision over Fin 4 against the fixed slice membership table.
Claim. For the causal tetrahedron type $(2,2)$, the set of vertices $v \in \{0,1,2,3\}$ with slice membership false (slice $t$) has cardinality $2$, and the set with membership true (slice $t+1$) has cardinality $2$.
background
This module opens the Lorentzian sector of the QG Seven-Gaps campaign. Prior discrete-gravity work in the stack is Euclidean; here the first certified CDT-style tetrahedron classes in $D=3$ are fixed, together with a Wick map on squared edge lengths.
Conventions follow Ambjørn–Jurkiewicz–Loll 3D CDT. Spatial slices are equilateral triangulations with squared length $a^2$. Between slices $t$ and $t+1$ one fills with two tetrahedron types: $(3,1)$ (three vertices on $t$, one on $t+1$) and $(2,2)$ (two on each). The inductive type CausalTetType names those two classes. Slice membership is the Boolean map sending each vertex in $\mathrm{Fin},4$ to false on slice $t$ and true on $t+1$: for $(2,2)$ the table is vertices ${0,1}$ on $t$ and ${2,3}$ on $t+1$.
Edge indexing is the standard Cayley–Menger order on four vertices. Timelike edges are exactly the cross-slice pairs; spacelike edges stay inside one slice. The present lemma only counts vertices per slice, not edges.
proof idea
One-line wrapper: decide. The universe of $\mathrm{Fin},4$ is finite, slice membership for type $(2,2)$ is a closed Boolean formula on the vertex index, and both filtered cardinalities are therefore decidable equalities to $2$. No external lemmas are invoked beyond the definition of the slice map.
why it matters
The count is the combinatorial backbone of the $(2,2)$ class in the Lorentzian CDT layer: it forces the edge multiset (two spacelike, four timelike) used by the subsequent timelike/spacelike edge-count lemmas and by the Wick involution $\alpha\mapsto -\alpha$ on squared lengths. Downstream siblings in the same module (timelike_count_twoTwo, spacelike_count_twoTwo, the cross-slice characterizations, and the non-degeneracy range for Euclideanized tets) all rest on this balanced bipartition of vertices.
In the broader Recognition stack this sits in the gravity/Seven-Gaps lane that supplies discrete Lorentzian kinematics before continuum limits. It does not itself touch the forcing chain T0–T8, the J-cost, or the phi ladder; it is pure CDT combinatorics that makes the later deficit-angle reality corollary at $\alpha=1$ well-typed. No parent theorem currently lists it in used_by; it is infrastructure for the module’s own edge-type and Wick theorems.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.