cm4_euclidean_threeTwo
plain-language theorem explainer
Exact closed form for the Euclideanized Cayley–Menger determinant of a CDT type-(3,2) 4-simplex: cm4 equals (12α−7)a⁸. Anyone checking non-degeneracy thresholds or matching Ambjørn–Jurkiewicz–Loll volumes cites this. The proof unfolds cm4 to the bordered 6×6 determinant, substitutes the explicit type-(3,2) edge matrix, and finishes by ring on the known 6×6 determinant.
Claim. For all real $a$ and $\alpha$, the 4-simplex Cayley–Menger determinant of the Euclideanized squared-edge data of a causal type-$(3,2)$ 4-simplex (three vertices on one spatial slice, two on the next) with spacelike scale $a$ and Euclideanized ratio $\alpha$ equals $(12\alpha-7)a^{8}$.
background
This module is Phase 3a of the QG Seven-Gaps Lorentzian lane: CDT-style causal 4-simplex classes in $D=4$, with Wick rotation as the algebraic continuation $\alpha\mapsto -\alpha$ on squared edge lengths. Spatial slices are equilateral tetrahedra of squared edge $a^{2}$. Between slices, type $(3,2)$ has three vertices on slice $t$ and two on $t+1$ (four spacelike and six timelike edges); type $(4,1)$ is the other class.
In the Euclideanized regime, spacelike squared lengths stay $a^{2}$ and the former timelike edges become $+\alpha a^{2}$ with $\alpha>0$. The quantity cm4 is the dimension-parametric Cayley–Menger determinant cmDetN at $n=4$: the determinant of the bordered $6\times 6$ matrix built from the ten squared distances. Classical volume satisfies $V^{2}\propto\mathrm{cm4}$; the AJL formula $V(3,2)=(a^{4}/96)\sqrt{12\alpha-7}$ is the cross-check that $9216 V^{2}=(12\alpha-7)a^{8}$.
proof idea
Term-mode, three steps. Unfold cm4 to cmDetN (the bordered Cayley–Menger determinant). Rewrite the matrix via the explicit Euclidean type-$(3,2)$ edge assignment cmMatrixN_euclidean_threeTwo, then replace its determinant by the closed form det_pentMatrix32. The remaining polynomial identity is discharged by ring, yielding $(12\alpha-7)a^{8}$.
why it matters
This is one of the two exact Euclidean evaluations that certify the 4D causal simplex machinery. Downstream, cm4_euclidean_pos_iff uses it to prove the sharp positivity criterion $\mathrm{cm4}>0\Leftrightarrow\alpha>\alpha_{\min}$ for type $(3,2)$; cm4_euclidean_degenerate_at_min plugs $\alpha=7/12$ to get exact degeneracy; cm4_euclidean_scale reads off the homogeneous $a^{8}$ weight. The status record causalSimplex4DStatus_flags marks cm4_thresholds_certified from these facts.
In the Recognition gravity lane this closes the Euclidean side of the kinematical Wick rotation for the $(3,2)$ class (the Lorentzian side is strict negativity of cm4). It does not yet touch the still-open action-level continuation flag. Landmark contact is local to the Seven-Gaps CDT lift rather than T0–T8 forcing.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.