cm3_euclidean_pos_iff
plain-language theorem explainer
For spatial edge scale a>0, a Euclideanized CDT tetrahedron of type (3,1) or (2,2) has strictly positive Cayley-Menger cubic (positive squared volume) exactly when the length-ratio parameter alpha exceeds the type-dependent threshold alphaMin. Discrete-gravity and CDT workers cite this for the sharp non-degeneracy window after Wick rotation. The proof cases on type and reduces each side to a sign comparison of a linear factor in alpha against a positive sixth power of a.
Claim. Fix $a>0$ and a causal tetrahedron class $\mathrm{ty}\in\{(3,1),(2,2)\}$. Let $E$ be the Euclideanized squared-edge assignment of that class at scale $a$ and ratio $\alpha$. Then the Cayley-Menger cubic of $E$ satisfies $\mathrm{CM}_3(E)>0$ if and only if $\alpha>\alpha_{\min}(\mathrm{ty})$, where $\alpha_{\min}$ is the hand-derived type threshold ($1/3$ for $(3,1)$, $1/2$ for $(2,2)$).
background
This module is the Lorentzian-sector lane of the QG Seven-Gaps campaign. Prior discrete-gravity results in the stack are Euclidean; here one builds certified 3D CDT tetrahedron classes and a kinematical Wick map on squared edge lengths.
Conventions follow Ambjørn-Jurkiewicz-Loll in $D=3$: spatial slices are equilateral triangulations with squared edge $a^2$. Between slices one fills with type $(3,1)$ (three vertices on $t$, one on $t+1$: three spacelike and three timelike edges) or type $(2,2)$ (two vertices per slice: two spacelike and four timelike). In the Lorentzian regime timelike squared lengths are $-\alpha a^2$ with $\alpha>0$; Wick rotation is the algebraic continuation $\alpha\mapsto -\alpha$, producing the Euclideanized edge tuple used here.
The Cayley-Menger cubic $\mathrm{CM}_3$ is the standard polynomial in the six squared edge lengths whose vanishing marks a flat (zero-volume) tetrahedron; positivity is the non-degeneracy certificate. Closed forms cm3_euclidean_threeOne / cm3_euclidean_twoTwo and the matching thresholds alphaMin are already certified upstream in the same module.
proof idea
First record $a^6>0$ from $a>0$. Case on the inductive causal type.
For $(3,1)$: rewrite with the closed form of $\mathrm{CM}3$ on the Euclideanized $(3,1)$ edges and with $\alpha{\min}=1/3$. Forward: if $\mathrm{CM}_3>0$ but $\alpha\le 1/3$, then $(1-3\alpha)a^6\ge 0$, contradicting the rewritten cubic by linarith. Reverse: if $\alpha>1/3$ then $(3\alpha-1)a^6>0$, and linarith yields $\mathrm{CM}_3>0$.
For $(2,2)$: same pattern with the $(2,2)$ closed form and $\alpha_{\min}=1/2$, comparing against the factor $(2\alpha-1)a^6$. No external lemmas beyond the two closed-form rewrites and elementary positivity of powers.
why it matters
This is the core exact-range non-degeneracy theorem of the causal-simplex Wick layer: both directions, not merely a sufficient bound. It discharges item 3 of the module program (non-degeneracy of Euclideanized simplices on a hand-derived parameter range) and underwrites the deficit-angle reality corollary at the physical point $\alpha=1$.
Downstream, the one-sided wrapper cm3_euclidean_pos is literally the .mpr direction of this iff, and the campaign ledger re-anchors proved gap flags against imported artifacts via campaign_flags_anchored. In the broader RS forcing chain the ambient dimension $D=3$ is the T8 landmark; the construction is the first certified Lorentzian edge-data layer sitting on that forced dimension, converting Euclidean Cayley-Menger control into a CDT-ready non-degeneracy window after Wick rotation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.