cm3_lorentzian_threeOne
plain-language theorem explainer
For a CDT type-(3,1) tetrahedron with spacelike squared length a² and timelike squared length −α a², the Cayley–Menger polynomial evaluates exactly to −2(3α+1)a⁶. Anyone proving Lorentzian non-realizability or preparing the Wick map to the Euclidean sector cites this identity. The proof substitutes the six edge values and finishes by ring algebra.
Claim. Let $a,\alpha\in\mathbb{R}$. For a type-$(3,1)$ causal tetrahedron whose squared edge lengths are $a^2$ on the three spacelike edges and $-\alpha a^2$ on the three timelike edges, the Cayley–Menger polynomial satisfies $\mathrm{CM}_3 = -2(3\alpha+1)a^6$.
background
This module opens the Lorentzian lane of the QG Seven-Gaps campaign in $D=3$ CDT (Ambjørn–Jurkiewicz–Loll). Spatial slices are equilateral triangulations with squared edge length $a^2$; spacetime between adjacent slices is filled by two tetrahedron classes. Type $(3,1)$ places three vertices on slice $t$ and one on $t+1$, giving three spacelike and three timelike edges (the time-reflected $(1,3)$ shares the same multiset).
Squared lengths follow the Lorentzian convention: spacelike edges carry $a^2$, timelike edges carry $-\alpha a^2$ with $\alpha>0$. The Cayley–Menger polynomial $\mathrm{cm3}$ is the explicit degree-three form in the six squared edge lengths from CayleyMengerPolynomial; classically $\mathrm{cm3}=288V^2$ on Euclidean-realizable tetrahedra, so its sign is the non-degeneracy interface used throughout the discrete-gravity stack.
Edge indexing is fixed: edges $0=(0,1)$, $1=(0,2)$, $3=(1,2)$ are the base triangle (spacelike); edges $2=(0,3)$, $4=(1,3)$, $5=(2,3)$ run to the apex (timelike).
proof idea
Term-mode calculation by direct substitution. Six have statements record the pointwise values of the Lorentzian squared-edge map on type $(3,1)$: indices $0,1,3$ equal $a^2$ and indices $2,4,5$ equal $-\alpha a^2$, each by rfl against the definition. Unfold cm3, rewrite the six slots, and close with ring. No external lemmas beyond the definitions of cm3 and lorentzianSqEdges.
why it matters
Feeds lorentzian_cm3_neg_threeOne, which reads the closed form to conclude $\mathrm{cm3}<0$ for all $\alpha\ge 0$ and $a>0$. That negativity is the certified statement that a Lorentzian $(3,1)$ tuple fails the Cayley–Menger non-degeneracy criterion, so it is not Euclidean-realizable; the Wick rotation ($\alpha\mapsto -\alpha$) is therefore mandatory to reach the Euclidean sector where NonDegenerateTet instances live.
In the module program this is step (2)–(3) of the Lorentzian layer: an exact algebraic identity on the causal class that unlocks the deficit-angle reality corollary at the physical point $\alpha=1$ and anchors the kinematical Wick map as a genuine continuation rather than a formal device. It sits inside the gravity Seven-Gaps campaign that lifts the entire prior Euclidean discrete-gravity stack into a certified Lorentzian regime, with $D=3$ matching the T8 spatial-dimension landmark of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.