slice_count_fourOne
plain-language theorem explainer
For the CDT (4,1) 4-simplex, exactly four of the five vertices lie on the earlier spatial slice and one on the later slice. Anyone checking the combinatorial edge census or Cayley–Menger setup for Lorentzian 4-simplices cites this. The proof is a pure `decide` on the finite Boolean assignment of vertices to slices.
Claim. For the causal 4-simplex of type $(4,1)$, the number of vertices $v\in\{0,1,2,3,4\}$ with slice membership equal to the earlier slice $t$ is $4$, and the number with membership equal to the later slice $t+1$ is $1$.
background
This module is the 4D Lorentzian lift of the 3D causal-simplex machinery: CDT-style 4-simplices fill the slab between adjacent spatial slices of equilateral tetrahedra. There are two combinatorial types. Type $(4,1)$ places four vertices on slice $t$ and one on $t+1$; type $(3,2)$ places three and two. Time reflections $(1,4)$ and $(2,3)$ share the same edge-length multisets.
Slice membership is the Boolean map sending each of the five vertices to false (slice $t$) or true (slice $t+1$). For type $(4,1)$ the definition is: vertex $4$ alone sits on $t+1$, and vertices $0,1,2,3$ sit on $t$. Spacelike edges stay inside a slice (squared length $a^2$); timelike edges cross slices (squared length $-\alpha a^2$ in the Lorentzian regime).
The count lemma is the first decide-able census that feeds the edge-type assignment (six spacelike, four timelike for $(4,1)$) and the later Cayley–Menger evaluations on both causal classes.
proof idea
One-line decide proof. The domain is Fin 5 and sliceOf for type $(4,1)$ is the Boolean predicate $v.val = 4$, so both filtered Finsets are finite and decidable; Lean closes the two cardinality equalities by exhaustive evaluation. No intermediate lemmas are invoked beyond the definition of slice membership.
why it matters
In the QG Seven-Gaps Lorentzian-sector lane (Phase 3a), the $(4,1)$ and $(3,2)$ classes are the elementary building blocks of 4D CDT between adjacent slices. This lemma locks the vertex census that the module docstring states in prose: four vertices on $t$, one on $t+1$. That census determines which of the ten lexicographic edges are cross-slice (timelike), which in turn fixes the squared-length multiset used by the Wick map $\alpha\mapsto -\alpha$ and by the bordered Cayley–Menger determinant cm4.
No downstream theorems currently depend on it in the graph, but sibling counts (timelike_count_fourOne, spacelike_count_fourOne, and the $(3,2)$ analogues) sit next to it as the combinatorial backbone for non-degeneracy thresholds and Lorentzian-side cm4 negativity. Framework-wise it is pure CDT kinematics in $D=4$ (Ambjørn–Jurkiewicz–Loll conventions), not a forcing-chain step; it supplies the discrete geometry that later gravity gaps will quote.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.