cm4_euclidean_pos
plain-language theorem explainer
For either CDT 4-simplex type, if the spatial edge scale a is positive and the asymmetry parameter alpha exceeds the type-dependent threshold (3/8 for (4,1), 7/12 for (3,2)), the Cayley–Menger determinant of the Euclideanized squared-edge tuple is strictly positive. Gravity and CDT workers cite this as the direct non-degeneracy certificate. The proof is a one-line application of the reverse direction of the exact positivity iff.
Claim. Let $\mathrm{ty}$ be a causal 4-simplex type ($(4,1)$ or $(3,2)$), and let $a,\alpha\in\mathbb{R}$ with $a>0$ and $\alpha>\alpha_{\min}(\mathrm{ty})$, where $\alpha_{\min}(4,1)=3/8$ and $\alpha_{\min}(3,2)=7/12$. Then the 4-simplex Cayley–Menger determinant of the Euclideanized squared-edge lengths is strictly positive: $\mathrm{CM}_4>0$.
background
This module is Phase 3a of the QG Seven-Gaps Lorentzian lane: causal (CDT-style) 4-simplex classes in $D=4$, with Wick rotation as an explicit map on the ten squared edge lengths. Spatial slices are equilateral tetrahedra of squared edge $a^2$. Between slices one fills with type $(4,1)$ (six spacelike + four timelike edges) or type $(3,2)$ (four spacelike + six timelike). In the Lorentzian regime timelike squared lengths are $-\alpha a^2$ with $\alpha>0$; Euclideanization is the continuation $\alpha\mapsto -\alpha$.
The quantity $\mathrm{cm4}$ is the bordered $6\times 6$ Cayley–Menger determinant from Geometry.CayleyMengerN, evaluated on those ten edges. Positivity of $\mathrm{cm4}$ is the non-degeneracy criterion used throughout (the 4D analogue of Regge tetrahedron non-degeneracy). The exact thresholds are packaged as $\alpha_{\min}$: $3/8$ for $(4,1)$ and $7/12$ for $(3,2)$.
The sibling iff cm4_euclidean_pos_iff already characterizes $\mathrm{cm4}>0$ exactly by $\alpha>\alpha_{\min}(\mathrm{ty})$ under $a>0$. This theorem is the forward half, stated for direct application.
proof idea
One-line term proof. Apply the reverse implication of cm4_euclidean_pos_iff ty a alpha ha, feeding the hypothesis $\alpha>\alpha_{\min}(\mathrm{ty})$. No further case split or arithmetic is needed here; the hard work lives in the iff.
why it matters
Direct non-degeneracy certificate for Euclideanized causal 4-simplices on the exact CDT range. Downstream, cm4_euclidean_pos_joint uses it twice to get simultaneous positivity for both types precisely when $\alpha>7/12$ (the standard 4d CDT Euclidean-regime bound). The packaged witness euclideanCausalPent installs this lemma as the cm_pos field of a NonDegeneratePent. The composite wick_lorentzian_nondegenerate rewrites the Wick image of a Lorentzian tuple back to the Euclidean edges and invokes this theorem, certifying the kinematical Wick rotation at the $\mathrm{cm4}$-criterion level.
In the Seven-Gaps campaign this closes the Euclidean non-degeneracy half of the 4D causal-simplex story (module goals 3–4). It does not yet upgrade $\mathrm{cm4}>0$ to geometric embeddability in $\mathbb{R}^4$; that step is classical and left unformalized.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.