alphaMin_lt_one
plain-language theorem explainer
For every 3D CDT causal tetrahedron type, the exact non-degeneracy threshold on the squared-length ratio alpha lies strictly below 1. Anyone packaging the physical-point Euclideanized simplex (unit spacing, alpha = 1) cites this inequality. The proof is a two-case numeric evaluation of the closed-form threshold.
Claim. For each causal tetrahedron type $\tau$ among the two 3D CDT classes ($(3,1)$ and $(2,2)$), the exact non-degeneracy threshold $\alpha_{\min}(\tau)$ satisfies $\alpha_{\min}(\tau) < 1$.
background
This module is the first certified Lorentzian layer of the QG Seven-Gaps campaign. Spatial slices are equilateral triangulations with squared edge length $a^2$. Between adjacent slices the fill is by two CDT tetrahedron types: $(3,1)$ (three vertices on slice $t$, one on $t+1$; three spacelike and three timelike edges) and $(2,2)$ (two vertices on each slice; two spacelike and four timelike edges). Timelike squared lengths are $-\alpha a^2$ in the Lorentzian regime ($\alpha > 0$); the Wick map continues $\alpha \mapsto -\alpha$.
Non-degeneracy of the Euclideanized simplex is controlled by the Cayley–Menger cubic $cm_3 > 0$ (positive squared volume). Hand computation yields an exact threshold $\alpha_{\min}(\tau)$ for each type: the Euclideanized tetrahedron is non-degenerate iff $\alpha > \alpha_{\min}(\tau)$. The physical CDT point is $\alpha = 1$ at unit spacing, so one must know that this point sits strictly above the threshold.
proof idea
Term-mode proof by exhaustive case split on the inductive type of causal tetrahedra. On each constructor the closed-form definition of the threshold is unfolded and discharged by norm_num, which evaluates the explicit rational (or algebraic) expression and checks the strict inequality against 1. No external lemmas are required beyond the definition of the threshold and the two constructors.
why it matters
This is the numeric gate that lets the physical point enter the non-degeneracy API. Downstream, physicalCausalTet builds a packaged non-degenerate Euclideanized causal tetrahedron at $a = 1$, $\alpha = 1$ by feeding this inequality into the general constructor. The same pattern is mirrored in 4D for causal pentachora. With the physical witness in hand, the module obtains the deficit-angle reality corollary at $\alpha = 1$: both Euclideanized types coincide with the regular tetrahedron, so dihedral angles are real. In the broader Recognition gravity lane this closes the kinematical Wick step of the Lorentzian sector (D = 3 spatial, eight-tick octave upstream) before dynamical or measure-theoretic claims.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.