cm3_euclidean_pos
plain-language theorem explainer
For either 3d CDT causal tetrahedron type, if the edge scale a is positive and the anisotropy alpha exceeds the type-dependent threshold, the Cayley-Menger polynomial on the Euclideanized squared edges is strictly positive. Gravity and CDT workers cite this as the direct non-degeneracy fact on the hand-derived range. The proof is a one-line application of the reverse direction of the characterizing iff.
Claim. Let $\tau$ be a 3d CDT causal tetrahedron type ($(3,1)$ or $(2,2)$), and let $a,\alpha\in\mathbb{R}$ satisfy $0<a$ and $\alpha>\alpha_{\min}(\tau)$. Then $0<\mathrm{CM}_3(e^2_{\mathrm{Euc}}(\tau,a,\alpha))$, where $e^2_{\mathrm{Euc}}$ are the Euclideanized squared edge lengths of that causal class and $\mathrm{CM}_3$ is the Cayley-Menger polynomial in six squared edges.
background
This module is the Lorentzian-sector lane of the QG Seven-Gaps campaign in $D=3$. Spatial slices are equilateral triangulations with squared edge length $a^2$; spacetime between adjacent slices is filled by two CDT tetrahedron types: $(3,1)$ (three vertices on slice $t$, one on $t+1$) and $(2,2)$ (two on each slice). Spacelike edges carry $a^2$; timelike edges carry $-\alpha a^2$ in the Lorentzian regime. The Euclideanization (Wick image) flips the timelike sign, equivalently the continuation $\alpha\mapsto -\alpha$ on the causal class.
Non-degeneracy of a tetrahedron is read from the Cayley-Menger polynomial $\mathrm{CM}_3$ in the six squared edge lengths: positivity of $\mathrm{CM}3$ (with positive squared edges) is the volume-squared criterion used by the existing Regge foundation. The type-dependent threshold $\alpha{\min}(\tau)$ is the exact lower bound, obtained by hand computation and certified in this module, above which the Euclideanized edge tuple is non-degenerate.
The present statement is the forward half of that characterization, packaged for direct use rather than as an iff.
proof idea
One-line term proof. It applies the reverse implication of the already-proved biconditional cm3_euclidean_pos_iff at the same (ty, a, alpha) and the hypothesis 0 < a, feeding in alphaMin ty < alpha to conclude 0 < cm3 (euclideanSqEdges ty a alpha). No further algebraic expansion of $\mathrm{CM}_3$ occurs at this site.
why it matters
This is the workhorse non-degeneracy fact for Euclideanized 3d CDT tets on the exact parameter range. Downstream, cm3_euclidean_pos_joint specializes it to both types at once on the standard CDT Euclidean-regime bound $\alpha>1/2$. The packaged definition euclideanCausalTet builds a NonDegenerateTet instance from it (positive squared edges plus $\mathrm{CM}_3>0$), tying the causal class into the existing Regge foundation. The composite wick_lorentzian_nondegenerate rewrites the Wick image of a Lorentzian causal tuple back to the Euclideanized edges and quotes this theorem, giving the certified kinematical Wick rotation: Lorentzian class member in, non-degenerate Euclidean tet out.
In the Seven-Gaps program this closes item 3 of the module brief (non-degeneracy on a hand-derived range) and underwrites the deficit-angle reality corollary at the physical point $\alpha=1$. It is pure 3d CDT kinematics; the forcing-chain landmarks (T5 J-cost, T7 eight-tick, T8 $D=3$) sit upstream of the discrete-gravity setting rather than inside this proof.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.