lorentzian_cm3_neg_threeOne
plain-language theorem explainer
The Lorentzian (3,1) CDT tetrahedron always has strictly negative Cayley-Menger determinant: for every spatial scale a>0 and every alpha≥0, cm3 of its squared-edge tuple is negative. Discrete-gravity and Wick-rotation workers cite this as the certified sign obstruction to Euclidean realizability in the Lorentzian sector. The proof rewrites to the closed cm3 formula for the (3,1) Lorentzian edges and finishes by positivity of a^6 and (3α+1).
Claim. For all real $a>0$ and $\alpha\ge 0$, if $e$ is the squared-edge 6-tuple of a Lorentzian type-$(3,1)$ causal tetrahedron (spacelike edges $a^2$, timelike edges $-\alpha a^2$), then the Cayley-Menger determinant satisfies $\mathrm{cm}_3(e)<0$.
background
This module is the Lorentzian-sector lane of the QG Seven-Gaps campaign. Prior discrete-gravity results in the stack are Euclidean; here the first certified Lorentzian layer is built for 3D CDT (Ambjørn-Jurkiewicz-Loll). Spatial slices are equilateral triangulations with squared edge length $a^2$. Between adjacent slices the filling tetrahedra are of two combinatorial types: (3,1) has three vertices on slice $t$ and one on $t+1$ (three spacelike and three timelike edges); (2,2) has two vertices on each slice.
In the Lorentzian regime, spacelike squared lengths are $a^2$ and timelike squared lengths are $-\alpha a^2$ with $\alpha\ge 0$. The Cayley-Menger polynomial $\mathrm{cm}_3$ is the classical 5×5 determinant on the six squared edge lengths; on a Euclidean-realizable tetrahedron it equals $288V^2$, so $\mathrm{cm}_3>0$ is the non-degeneracy interface used by NonDegenerateTet. The sibling map lorentzianSqEdges builds the (3,1) or (2,2) squared-edge tuple from $(a,\alpha)$.
The classical reading of $\mathrm{cm}_3<0$ is therefore "not Euclidean-realizable." The module's Wick rotation is the algebraic continuation $\alpha\mapsto -\alpha$ on those tuples, and is needed to reach the Euclidean sector.
proof idea
Term-mode proof in four steps. First rewrite by the closed identity cm3_lorentzian_threeOne, which evaluates $\mathrm{cm}_3$ on the Lorentzian (3,1) edge tuple to an explicit multiple of $-(3\alpha+1)a^6$ (up to a positive combinatorial constant absorbed by the rewrite). Next, $a>0$ gives $a^6>0$ by pow_pos. Then $3\alpha+1>0$ (from $\alpha\ge 0$) and the product rule yield $(3\alpha+1)a^6>0$. A final linarith closes the strict inequality $\mathrm{cm}_3<0$.
why it matters
This is the certified sign fact that Lorentzian (3,1) simplices fail the Cayley-Menger non-degeneracy criterion for the entire physical parameter range. It underwrites the module claim that a genuine Wick rotation is required to reach the Euclidean sector, rather than a mere reparametrization. Downstream it feeds the Euclideanized non-degeneracy and deficit-angle reality results in the same file (including the (2,2) Euclidean cm3 identity and the NonDegenerateTet instances on the hand-derived alpha range). In the broader Recognition gravity program it is a kinematical lemma on the Lorentzian side of the D=3 discrete geometry stack, complementary to the Euclidean Regge/Cayley-Menger foundation already formalized upstream. It does not itself compute volumes or curvature; it only locks the sign obstruction that forces the Wick bridge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.