alphaMin
plain-language theorem explainer
Exact non-degeneracy thresholds for the two 3D CDT tetrahedron classes after Euclideanization: 1/3 for type (3,1) and 1/2 for type (2,2). Anyone proving Cayley–Menger positivity or deficit-angle reality on the Wick-rotated simplex cites these constants. The definition is a pure case split on causal type.
Claim. For each causal tetrahedron type in 3D CDT, the exact non-degeneracy threshold is $\alpha_{\min}(3,1)=1/3$ and $\alpha_{\min}(2,2)=1/2$. Euclideanized simplices are non-degenerate precisely when the timelike-to-spacelike squared-length ratio $\alpha$ exceeds this type-dependent floor.
background
This module opens the Lorentzian sector of the QG Seven-Gaps campaign. Spatial slices are equilateral triangulations with squared edge length $a^2$; spacetime between adjacent slices is filled by two CDT tetrahedron classes. Type (3,1) has three vertices on slice $t$ and one on $t+1$ (three spacelike, three timelike edges); type (2,2) has two vertices on each slice (two spacelike, four timelike). Timelike squared lengths are $-\alpha a^2$ in the Lorentzian regime ($\alpha>0$); Wick rotation continues $\alpha\mapsto -\alpha$.
Non-degeneracy of the Euclideanized simplex is controlled by the Cayley–Menger polynomial on the six squared edge lengths. Hand computation yields sharp lower bounds on $\alpha$ below which the volume (or CM positivity) collapses. The parallel 4D definition uses thresholds $3/8$ and $7/12$ for the pentatope classes; the present constants are the 3D analogues.
proof idea
Pure definition by cases on the inductive type of causal tetrahedra. No proof obligations: type (3,1) maps to $1/3$, type (2,2) maps to $1/2$. Downstream lemmas discharge equalities by rfl and positivity or comparison facts by norm_num on these literals.
why it matters
These thresholds anchor the non-degeneracy theorem for Euclideanized causal tetrahedra and the deficit-angle reality corollary at the physical point $\alpha=1$. They feed the campaign ledger anchor (one load-bearing result per gap re-derived from imported modules) and the parallel 4D alphaMin infrastructure (positivity, strict inequality below 1, and the iff statement that CM positivity holds exactly when $\alpha$ exceeds the type-dependent floor). Within Recognition Science gravity, they certify the first Lorentzian layer after an entirely Euclidean discrete-gravity stack, tying the Wick map and CDT edge combinatorics to an exact, hand-derived parameter range rather than a numerical search.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.