cm4_lorentzian_fourOne
plain-language theorem explainer
Exact closed form for the 4-simplex Cayley-Menger determinant on a Lorentzian type-(4,1) causal simplex: cm4 equals -((8α+3)a^8). Cited by anyone proving Lorentzian cm4-negativity or Wick-rotation thresholds in the 4D CDT lane. Proof unfolds the determinant definition, substitutes the precomputed (4,1) matrix and its det, then finishes by ring.
Claim. For all real $a$ and $\alpha$, the sign-normalized 4-simplex Cayley-Menger determinant of the Lorentzian squared-edge lengths of causal type $(4,1)$ (four vertices on slice $t$, one on $t+1$) equals $-((8\alpha+3)a^{8})$.
background
This module is Phase 3a of the QG Seven-Gaps Lorentzian-sector lane: 4D CDT-style causal 4-simplices between adjacent spatial slices, with Wick rotation as the algebraic continuation $\alpha\mapsto -\alpha$ on squared edge lengths. Type $(4,1)$ has four vertices on slice $t$ and one on $t+1$ (six spacelike edges of squared length $a^2$, four timelike edges of squared length $-\alpha a^2$ in the Lorentzian regime).
The object cm4 is the sign-normalized 4-simplex Cayley-Menger determinant, defined as $-\mathrm{cmDetN}$ of the bordered distance matrix so that $\mathrm{cm4}>0$ on non-degenerate Euclidean 4-simplices and $\mathrm{cm4}=9216 V^2$. Upstream, cmDetN is the dimension-parametric determinant from Geometry.CayleyMengerN; the local lemmas cmMatrixN_lorentzian_fourOne and det_pentMatrix41 supply the explicit Lorentzian matrix and its closed-form determinant for type $(4,1)$.
proof idea
Term-mode, three steps. Unfold cm4 and cmDetN to expose the bordered matrix determinant. Rewrite with cmMatrixN_lorentzian_fourOne (the explicit 6×6 Cayley-Menger matrix on the Lorentzian $(4,1)$ edge tuple) and det_pentMatrix41 (its closed-form determinant). Finish with ring to match $-((8\alpha+3)a^8)$.
why it matters
This is the exact evaluation that powers the Lorentzian non-positivity theorem for type $(4,1)$. Downstream, lorentzian_cm4_neg_fourOne rewrites with this identity and concludes $\mathrm{cm4}<0$ for all $\alpha\ge 0$ and $a>0$, i.e. the Lorentzian $(4,1)$ tuple always fails the Cayley-Menger positivity criterion. Under the classical reading ($\mathrm{cm4}>0$ iff embeddable in $\mathbb{R}^4$), that forces a genuine Wick rotation to reach the Euclidean sector. The module pairs this with the type-$(3,2)$ companion and the Euclidean non-degeneracy thresholds in $\alpha$, closing the kinematical 4D lift of the earlier 3D causal-simplex Wick machinery. Framework context: D=4 spacetime simplices in the gravity/CDT lane of the Seven-Gaps campaign (not the T8 D=3 spatial forcing step).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.