cm4_euclidean_fourOne
plain-language theorem explainer
For a Euclideanized type-(4,1) causal 4-simplex with spatial scale a and edge-ratio parameter α, the bordered Cayley–Menger determinant equals (8α−3)a⁸. CDT and discrete-gravity workers cite this as the exact volume-squared polynomial for the (4,1) class. The proof unfolds cm4 to the 6×6 determinant, substitutes the closed-form edge matrix and its determinant, then finishes by ring.
Claim. For all real $a$ and $\alpha$, if $D$ is the ten squared edge lengths of a type-$(4,1)$ causal 4-simplex after Euclideanization (spacelike edges $a^2$, former-timelike edges $\alpha a^2$), then the 4-simplex Cayley–Menger determinant satisfies $\mathrm{CM}_4(D)=(8\alpha-3)a^8$. Equivalently, $9216\,V(4,1)^2=(8\alpha-3)a^8$ with the Ambjørn–Jurkiewicz–Loll volume $V(4,1)=(a^4/96)\sqrt{8\alpha-3}$.
background
This module is Phase 3a of the QG Seven-Gaps Lorentzian lane: the 4D CDT lift of the 3D causal-simplex Wick machinery. Between adjacent spatial slices one fills spacetime with two 4-simplex types. Type (4,1) places four vertices on slice $t$ and one on $t+1$ (six spacelike edges, four timelike); type (3,2) is the complementary split. Spacelike squared lengths are $a^2$; Lorentzian timelike squared lengths are $-\alpha a^2$ with $\alpha>0$. Euclideanization is the algebraic continuation $\alpha\mapsto -\alpha$ on those edges (equivalently the Wick map on the ten-edge length vector).
The quantity $\mathrm{cm4}$ is the dimension-parametric Cayley–Menger determinant $\mathrm{cmDetN}$ at $n=4$: the determinant of the bordered $6\times 6$ matrix built from squared distances. Classically $V_4^2=(-1)^{5}\det(\mathrm{CM})/(2^4(4!)^2)$, so positivity of $\mathrm{cm4}$ is the algebraic non-degeneracy test used throughout the module. The AJL formula $V(4,1)=(a^4/96)\sqrt{8\alpha-3}$ is the geometric cross-check quoted in the doc-comment.
proof idea
Term-mode, three steps. Unfold $\mathrm{cm4}$ to $\mathrm{cmDetN}$. Rewrite the bordered matrix via the specialized evaluation cmMatrixN_euclidean_fourOne (the Euclidean type-(4,1) edge assignment) and replace its determinant by the closed form det_pentMatrix41. The resulting polynomial identity is discharged by ring, yielding $(8\alpha-3)a^8$. No case splits or analytic estimates.
why it matters
Exact evaluation for the (4,1) class is the algebraic engine under the module’s core non-degeneracy theorems. Downstream, cm4_euclidean_pos_iff rewrites through this identity to get $\mathrm{cm4}>0\Leftrightarrow\alpha>\alpha_{\min}$ for type (4,1); cm4_euclidean_degenerate_at_min plugs $\alpha=3/8$ to obtain exact vanishing; cm4_euclidean_scale reads off the $a^8$ homogeneity; cm4_regular_unit recovers the classical regular unit value $\mathrm{cm4}=5$ at $\alpha=1$. The status record causalSimplex4DStatus_flags marks cm4_thresholds_certified from these facts. Outside the module, causalPent_metric_observable_varies uses the same evaluation to show that combinatorial type alone does not fix the 4-volume observable. In the Seven-Gaps campaign this closes the Euclidean CM side of the 4D kinematical Wick rotation; the status flag still records action-level continuation as open. Landmark contact is T8 ($D=3$ spatial slices feeding 4D simplices) and the CDT (4,1)/(3,2) classification, not the J-cost or $\phi$-ladder chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.