alphaMin_threeOne
plain-language theorem explainer
The non-degeneracy threshold for a (3,1) causal tetrahedron is exactly one-third: after Wick rotation to Euclidean signature, the Cayley–Menger volume vanishes at α = 1/3 and is positive strictly above it. Anyone citing the exact 3d CDT Euclidean regime bound or the joint (3,1)+(2,2) non-degeneracy window needs this constant. The proof is definitional reflexivity.
Claim. For the (3,1) causal tetrahedron class (three vertices on slice $t$, one on slice $t+1$), the exact non-degeneracy threshold equals $1/3$: $\alpha_{\min}(3,1) = 1/3$.
background
This module opens the Lorentzian sector of the QG Seven-Gaps campaign in $D=3$. Spatial slices are equilateral triangulations with squared edge length $a^2$; the spacetime between adjacent slices is filled by two CDT tetrahedron types. Type (3,1) has three vertices on slice $t$ and one on $t+1$ (three spacelike edges of length squared $a^2$, three timelike edges of length squared $-\alpha a^2$ in the Lorentzian regime). Type (2,2) has two vertices on each slice.
The Wick rotation is the algebraic continuation $\alpha\mapsto -\alpha$ on squared timelike lengths. Non-degeneracy of the Euclideanized simplex is controlled by the Cayley–Menger polynomial $\mathrm{cm}_3$: the simplex has positive squared volume precisely when $\mathrm{cm}_3>0$. The definition alphaMin packages the hand-derived exact thresholds: $1/3$ for (3,1) and $1/2$ for (2,2). The 4d analogue records the parallel constants $3/8$ and $7/12$ for the pentachoron classes.
proof idea
One-line definitional equality. The function alphaMin is defined by pattern-match on the inductive type of causal tetrahedra, sending the (3,1) constructor to the literal rational $1/3$. The theorem is therefore rfl.
why it matters
Pins the exact lower edge of the Euclidean non-degeneracy window for (3,1) tetrahedra. Downstream, cm3_euclidean_pos_iff rewrites with this equality to obtain the biconditional $0<\mathrm{cm}_3\leftrightarrow\alpha>1/3$; cm3_euclidean_degenerate_at_min uses it to prove vanishing of $\mathrm{cm}_3$ exactly at the threshold; and cm3_euclidean_pos_joint combines it with the (2,2) threshold $1/2$ to recover the standard 3d CDT bound that both types are simultaneously non-degenerate for $\alpha>1/2$. This is the kinematical foundation for the deficit-angle reality corollary at the physical point $\alpha=1$ and for any later Regge or CDT curvature estimates in the Lorentzian sector. It sits in the gravity lane of the Seven-Gaps campaign; the spatial dimension $D=3$ is the T8 landmark of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.