cm3_lorentzian_twoTwo
plain-language theorem explainer
For a causal (2,2) tetrahedron with spatial spacing a and timelike parameter alpha, the Cayley-Menger polynomial on the Lorentzian squared-edge tuple equals -(4(2 alpha + 1) a^6). Discrete-gravity and CDT workers cite this closed form when checking non-degeneracy or sign of the 4-volume proxy. The proof substitutes the six edge values and finishes by ring.
Claim. For all real $a$ and $\alpha$, if $e$ is the squared-edge 6-tuple of a type-$(2,2)$ causal tetrahedron (two vertices per adjacent spatial slice) with spacelike squared lengths $a^2$ and timelike squared lengths $-\alpha a^2$, then the Cayley-Menger polynomial satisfies $\mathrm{CM}_3(e) = -4(2\alpha+1)a^6$.
background
This module opens the Lorentzian sector of the QG Seven-Gaps campaign in 3D CDT (Ambjørn-Jurkiewicz-Loll). Spatial slices are equilateral triangulations with squared edge length $a^2$. Between slices $t$ and $t+1$ one fills with two tetrahedron classes: type $(3,1)$ (three vertices on one slice, one on the other) and type $(2,2)$ (two vertices on each slice).
For type $(2,2)$, vertices ${0,1}$ sit on slice $t$ and ${2,3}$ on $t+1$. With the standard edge indexing $0=(0,1),\ldots,5=(2,3)$, that yields two spacelike edges (indices $0,5$) carrying $a^2$ and four timelike edges (indices $1$--$4$) carrying $-\alpha a^2$ in the Lorentzian regime $\alpha>0$. The map lorentzianSqEdges packages exactly this assignment.
The Cayley-Menger polynomial cm3 is the explicit degree-3 form in the six squared lengths that (up to a universal factor) recovers $288 V^2$ for a Euclidean tetrahedron. Here it is evaluated on the Lorentzian tuple as an algebraic identity, before any positivity or non-degeneracy hypotheses.
proof idea
Term-style calculation by direct substitution. Six have steps record the edge values of lorentzianSqEdges on type twoTwo by rfl: indices $0$ and $5$ equal $a^2$, indices $1$--$4$ equal $-\alpha a^2$. Unfold cm3, rewrite those six equalities into the polynomial, and close with ring. No external lemmas beyond the definitions of cm3 and the edge map.
why it matters
Gives the exact Lorentzian $\mathrm{CM}_3$ for the $(2,2)$ class, the second of the two CDT tetrahedron types in $D=3$. Downstream, lorentzian_cm3_neg_twoTwo rewrites with this identity and concludes $\mathrm{CM}_3<0$ whenever $a>0$ and $\alpha\ge 0$, feeding the non-degeneracy and deficit-angle reality lane of the module (including the physical point $\alpha=1$).
In the broader Recognition gravity stack this is kinematical scaffolding for the Lorentzian sector: every prior discrete-gravity result in the monolith was Euclidean; the Wick lane treats $\alpha\mapsto -\alpha$ as algebraic continuation on the causal class. The closed form is the $(2,2)$ counterpart of the $(3,1)$ evaluation and is needed before certified volume signs or Regge deficit angles can be stated in Lorentzian signature. It does not itself invoke the forcing chain (T0--T8) or the mass ladder; it sits in the geometry layer those later gravity claims consume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.