cm3_euclidean_threeOne
plain-language theorem explainer
For a type-(3,1) CDT tetrahedron after Euclideanization, the Cayley–Menger determinant collapses to the closed form $2(3\alpha-1)a^6$. Gravity and discrete-QG workers cite it to read off exact non-degeneracy thresholds in the Wick-rotated sector. The proof substitutes the six squared edge lengths and finishes by polynomial ring normalization.
Claim. For all real $a$ and $\alpha$, if the six squared edge lengths of a type-$(3,1)$ causal tetrahedron are Euclideanized so that the three base (spacelike) edges equal $a^2$ and the three legs equal $\alpha a^2$, then the Cayley–Menger determinant of that edge sextuple equals $2(3\alpha-1)a^6$.
background
This module opens the Lorentzian lane of the QG Seven-Gaps campaign in $D=3$. Prior discrete-gravity results in the stack are Euclidean; here causal tetrahedra are classified CDT-style and Wick-rotated by flipping the sign of timelike squared lengths (equivalently $\alpha\mapsto -\alpha$ on the causal class).
Type $(3,1)$ places three vertices on slice $t$ and one on $t+1$: three spacelike edges of squared length $a^2$ form an equilateral base, and three legs (timelike before Wick rotation) carry squared length $\alpha a^2$ after Euclideanization. Edge indexing follows the Cayley–Menger polynomial convention: edges $0=(0,1)$, $1=(0,2)$, $2=(0,3)$, $3=(1,2)$, $4=(1,3)$, $5=(2,3)$, with base ${0,1,3}$ and legs ${2,4,5}$.
The scalar cm3 is the Cayley–Menger determinant of a tetrahedron from its six squared edge lengths; its sign and vanishing control oriented volume and degeneracy of the Euclideanized simplex.
proof idea
Six definitional facts pin the Euclideanized edge map on type $(3,1)$: indices $0,1,3$ equal $a^2$ and indices $2,4,5$ equal $\alpha a^2$. Unfold the Cayley–Menger polynomial, rewrite those six slots, and close with ring. No external lemmas are required; the identity is pure polynomial arithmetic on the substituted monomials, matching the hand count that three balanced terms contribute $\alpha(1+\alpha)a^6$ each and four monomials contribute $(1+3\alpha^2)a^6$, netting $2(3\alpha-1)a^6$.
why it matters
Exact closed form for the Euclideanized $(3,1)$ volume polynomial is the algebraic engine behind the module’s non-degeneracy lane. Downstream, cm3_euclidean_pos_iff rewrites through this identity to prove that for $a>0$ one has $\mathrm{cm3}>0$ if and only if $\alpha>\alpha_{\min}$ for type $(3,1)$, and cm3_euclidean_degenerate_at_min plugs $\alpha=\alpha_{\min}$ to get exact vanishing. Together they certify the hand-derived threshold range and feed NonDegenerateTet instances plus the deficit-angle reality corollary at the physical point $\alpha=1$.
In the broader Recognition stack this is kinematical scaffolding for Lorentzian Regge/CDT geometry in the forced $D=3$ spatial setting (forcing chain T8), not a dynamical Einstein equation. It converts combinatorial edge typing into a concrete polynomial test that the Wick-rotated simplex is non-degenerate on an exact half-line in $\alpha$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.