slice_count_threeOne
plain-language theorem explainer
Type (3,1) causal tetrahedra place three vertices on slice t and one on slice t+1. Anyone building the Lorentzian CDT edge-type or Wick layer cites this for the combinatorial slice partition of Fin 4. The proof is a one-line decide on a finite Boolean filter.
Claim. For the causal tetrahedron type $(3,1)$, among the four vertices $\{0,1,2,3\}$, exactly three satisfy $\mathrm{slice}=t$ and exactly one satisfies $\mathrm{slice}=t+1$.
background
This module opens the Lorentzian sector of the QG Seven-Gaps campaign. Prior discrete-gravity results in the stack are Euclidean; here the first certified Lorentzian layer is built for 3d CDT (Ambjorn-Jurkiewicz-Loll): two tetrahedron classes between adjacent spatial slices, a Wick map on squared edge lengths, and non-degeneracy of the Euclideanized simplices.
Spatial slices are 2d equilateral triangulations. Between slices $t$ and $t+1$ one fills with type $(3,1)$ (three vertices on $t$, one on $t+1$) and type $(2,2)$ (two on each). The inductive type CausalTetType names those two classes. Slice membership is the Boolean map sending a vertex in $\mathrm{Fin},4$ to false on slice $t$ and true on $t+1$: for $(3,1)$ it is true exactly when the vertex index equals 3.
Vertex indexing follows the Cayley-Menger convention (vertices $0,1,2,3$). The companion 4d simplex module uses the same slice-membership pattern on $\mathrm{Fin},5$; the present lemma is the 3d tetrahedron case.
proof idea
Pure decidability. The universe of $\mathrm{Fin},4$ is finite, sliceOf for type $(3,1)$ is the Boolean predicate $v\mapsto(v=3)$, and both filtered cardinalities are closed terms. The tactic decide evaluates the two equalities and discharges the conjunction. No lemmas are invoked beyond the definitional unfolding of sliceOf and Finset cardinality on a decidable filter.
why it matters
The combinatorial slice counts are the first certified facts in the Lorentzian CDT layer. They underwrite the edge-type assignment (an edge is timelike iff its endpoints lie on different slices) and therefore the squared-length dictionary used by the Wick involution $\alpha\mapsto -\alpha$. Downstream siblings in the same module (isTimelike_threeOne_eq_crossSlice, timelike_count_threeOne, spacelike_count_threeOne, and the Wick non-degeneracy theorems) rest on this partition: three spacelike edges among the $t$-slice triangle plus three timelike edges to the apex.
In the broader Recognition stack this is kinematical scaffolding for discrete gravity in $D=3$ (forcing-chain landmark T8), not a dynamical claim. No parent theorem currently imports it (used_by is empty); it is a leaf that closes the decide-able slice arithmetic before the algebraic Wick and deficit-angle work.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.