cm4
plain-language theorem explainer
Sign-normalized 4-simplex Cayley–Menger determinant on ten squared edge lengths, equal to 9216 times squared 4-volume. Positivity marks non-degenerate Euclidean 4-simplices. CDT and discrete-gravity workers cite it for exact Euclidean-regime thresholds on causal (4,1) and (3,2) classes. Defined by packaging edges into the n=4 distance record and negating the generic bordered determinant.
Claim. For a 4-simplex with squared edge lengths $x\in\mathbb{R}^{10}$ (lexicographic order on the ten pairs among five vertices), set $\mathrm{CM}_4(x):=-\det(\mathrm{CM}(D(x)))$, where $D(x)$ is the Cayley–Menger squared-distance package of $x$. The sign is chosen so that $\mathrm{CM}_4=9216\,V^2$ on Euclidean 4-simplices, hence $\mathrm{CM}_4>0$ on non-degenerate Euclidean ones.
background
In 4D causal dynamical triangulations (Ambjørn–Jurkiewicz–Loll), spatial slices are equilateral tetrahedral complexes with squared edge length $a^2$. Between slices $t$ and $t+1$ the fill is by two 4-simplex types: (4,1) with six spacelike and four timelike edges, and (3,2) with four spacelike and six timelike edges. Timelike squared lengths are $-\alpha a^2$ Lorentzian ($\alpha>0$); Wick rotation continues $\alpha\mapsto -\alpha$.
Squared edges are a map $\mathrm{Fin},10\to\mathbb{R}$. Upstream, the dimension-parametric Cayley–Menger determinant is $\det$ of the bordered distance matrix, with classical formula $V_n^2=(-1)^{n+1}\det(\mathrm{CM})/(2^n(n!)^2)$. For $n=4$ the denominator is $9216=2^4(4!)^2$; the present definition absorbs the remaining sign by a leading minus so positivity matches Euclidean non-degeneracy.
proof idea
One-line definition. Package the ten squared lengths into a SimplexSquaredDistances 4 record (symmetry and zero diagonal by finite case analysis), evaluate the generic bordered determinant cmDetN, and negate. The minus aligns the classical sign convention so Euclidean non-degenerate simplices give a positive value equal to $9216 V^2$. No further algebraic work lives in the definition itself.
why it matters
Volume probe for the QG Seven-Gaps Lorentzian-sector Phase 3a (kinematical Wick rotation in 4D). Downstream exact evaluations give $\mathrm{CM}4=(8\alpha-3)a^8$ on Euclideanized (4,1), matching the AJL volume $V{(4,1)}=(a^4/96)\sqrt{8\alpha-3}$ via $9216 V^2$. The positivity criterion $\mathrm{CM}4>0$ iff $\alpha>\alpha{\min}(\mathrm{type})$ yields joint non-degeneracy of both causal classes precisely for $\alpha>7/12$, the standard 4d CDT Euclidean bound; degeneracy is exact at threshold. Feeds the core range theorems, scale and joint positivity lemmas, and the Lorentzian-side negativity story. Discrete-geometry kinematics in the gravity lane; not a T0–T8 forcing step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.