timelike_count_fourOne
plain-language theorem explainer
In 4D CDT, a (4,1) simplex (four vertices on one spatial slice, one on the adjacent slice) has exactly four timelike edges among its ten edges. Combinatorial checks of Lorentzian edge-type assignments cite this count. The proof is a single `decide` over the finite Boolean filter on Fin 10.
Claim. Among the ten edges of a causal 4-simplex of type $(4,1)$ (four vertices on slice $t$, one on slice $t+1$), exactly four edges are timelike: $\#\{e \in \{0,\ldots,9\} : e\text{ is timelike for type }(4,1)\} = 4$.
background
This module is Phase 3a of the QG Seven-Gaps Lorentzian lane: the 4D CDT lift of the 3D causal-simplex machinery. Between adjacent spatial slices one fills spacetime with two 4-simplex types. Type $(4,1)$ places four vertices on slice $t$ and one apex on $t+1$; type $(3,2)$ places three and two. Edges are indexed lexicographically as Fin 10.
Spacelike edges carry squared length $a^2$; timelike edges carry $-\alpha a^2$ ($\alpha>0$) in the Lorentzian regime. The predicate isTimelike marks an edge true precisely when it joins the two slices. For type $(4,1)$ those are the four edges touching the apex (indices ${3,6,8,9}$), matching the Ambjorn–Jurkiewicz–Loll convention of 6 spacelike + 4 timelike edges.
The sibling count lemmas (slice_count_fourOne, spacelike_count_fourOne, and the $(3,2)$ analogues) form the same decide-able combinatorial layer.
proof idea
One-line decidability proof. The universe Finset.univ on Fin 10 is finite, isTimelike CausalPentType.fourOne is a closed Boolean combination of equality tests on e.val, and equality of the filtered cardinality to 4 is a decidable Prop. Lean discharges it by decide with no lemmas and no arithmetic.
why it matters
The module builds four pillars: causal class edge-type assignment, Wick rotation as an involution acting by $\alpha\mapsto -\alpha$, exact Cayley–Menger cm4 on both classes, and Euclidean non-degeneracy thresholds. This theorem locks the first pillar for type $(4,1)$: the timelike count is exactly 4, as required by the CDT convention stated in the module doc.
No downstream theorems yet list this declaration as a dependency (used_by is empty), but the parallel spacelike count and the $(3,2)$ counts sit beside it; together they underwrite the squared-length assignment that the Wick map and cm4 evaluations consume. In the broader Recognition forcing chain the result is kinematical scaffolding for $D=4$ Lorentzian geometry rather than a T0–T8 step, yet it is the combinatorial gate that lets the 4D Cayley–Menger and Wick-rotation theorems run on a verified edge partition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.