lorentzian_cm4_neg_fourOne
plain-language theorem explainer
For every spatial scale a>0 and Lorentzian parameter α≥0, the Cayley-Menger determinant of a causal (4,1) 4-simplex with Lorentzian squared edge lengths is strictly negative. Cited by anyone arguing Lorentzian CDT (4,1) simplices fail Euclidean realizability and that a Wick rotation is required. Proof rewrites to a closed form and discharges the sign by positivity of a⁸ and of (8α+3).
Claim. For all real $a>0$ and $\alpha\ge 0$, if the ten squared edge lengths of a causal type-$(4,1)$ 4-simplex are assigned in the Lorentzian regime (six spacelike edges of squared length $a^2$, four timelike edges of squared length $-\alpha a^2$), then the bordered Cayley-Menger determinant satisfies $\mathrm{cm}_4<0$.
background
This module is the 4D Lorentzian lift in the QG Seven-Gaps campaign (Phase 3a): causal dynamical triangulation (CDT) 4-simplices between adjacent spatial slices, following Ambjørn–Jurkiewicz–Loll conventions. Spatial slices are equilateral tetrahedra of squared edge length $a^2$. Between slices one fills with two combinatorial types; type $(4,1)$ places four vertices on slice $t$ and one on $t+1$ (six spacelike and four timelike edges; the time reflection $(1,4)$ shares the same edge multiset).
In the Lorentzian regime, spacelike squared lengths are $a^2$ and timelike squared lengths are $-\alpha a^2$ with $\alpha\ge 0$. The object $\mathrm{cm}_4$ is the 4-simplex Cayley-Menger determinant, realized as the bordered $6\times 6$ determinant from the dimension-parametric cmDetN. Classical geometry reads $\mathrm{cm}_4>0$ as the criterion for Euclidean embeddability in $\mathbb{R}^4$; that classical equivalence is not formalized here for $n=4$.
The companion exact evaluation on Lorentzian $(4,1)$ edges supplies the closed form used below; the Euclidean-side evaluations give nondegeneracy thresholds in $\alpha$ for both causal types.
proof idea
Term-mode proof in four steps. First rewrite by the exact closed-form evaluation of $\mathrm{cm}_4$ on Lorentzian $(4,1)$ squared edges, which reduces the goal to a sign claim on an explicit polynomial in $a$ and $\alpha$ (a negative multiple of $(8\alpha+3)a^8$). Then $a^8>0$ by pow_pos from $a>0$. Next $(8\alpha+3)a^8>0$ by mul_pos, using $8\alpha+3>0$ from $\alpha\ge 0$ via linarith. A final linarith discharges $\mathrm{cm}_4<0$.
why it matters
Closes the Lorentzian-side half of item 4 in the module program: strict $\mathrm{cm}_4$ negativity on the Lorentzian sector for type $(4,1)$, matching the Euclidean nondegeneracy thresholds already evaluated for both causal classes. The doc-comment states the intended reading: under the classical Cayley-Menger realizability theorem ($\mathrm{cm}_4>0$ iff embeddable in $\mathbb{R}^4$), this sign fact means Lorentzian $(4,1)$ data are never Euclidean-realizable, so the kinematical Wick rotation ($\alpha\mapsto -\alpha$ on the causal class, proved as an involution elsewhere in the module) is genuinely required to reach the Euclidean sector.
That upgrade is explicitly out of scope here; the 3D analog lives in Geometry/TetrahedronRealization.lean, and the $n=4$ classical theorem is not in the repo. The result sits in the Lorentzian-sector lane of the Seven-Gaps gravity campaign and underwrites the claim that CDT 4-simplex kinematics force a Wick step before Euclidean measure theory applies. A parallel sign theorem for Lorentzian $(3,2)$ is stated immediately below.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.