alphaMin_pos
plain-language theorem explainer
For both 3d CDT tetrahedron types ((3,1) and (2,2)), the exact non-degeneracy threshold α_min is strictly positive (1/3 and 1/2 respectively). Anyone packaging a Euclideanized causal tetrahedron as a NonDegenerateTet cites this to chain α_min < α into 0 < α. The proof is a two-case split with numerical evaluation of the definition.
Claim. For every causal tetrahedron type $\tau\in\{(3,1),(2,2)\}$, the non-degeneracy threshold satisfies $0 < \alpha_{\min}(\tau)$, where $\alpha_{\min}(3,1)=1/3$ and $\alpha_{\min}(2,2)=1/2$.
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 classes: type (3,1) (three vertices on slice $t$, one on $t+1$; 3 spacelike + 3 timelike edges) and type (2,2) (two vertices on each slice; 2 spacelike + 4 timelike). Timelike squared lengths are $-\alpha a^2$ with $\alpha>0$; Wick rotation continues $\alpha\mapsto -\alpha$.
The local definition alphaMin records the exact hand-derived non-degeneracy thresholds: $1/3$ for (3,1) and $1/2$ for (2,2). Above these values the Euclideanized squared-edge assignment has all edges positive and positive Cayley–Menger volume $cm_3$. The 4d sibling module uses the analogous thresholds $3/8$ and $7/12$ for pentachoron types.
proof idea
One-line wrapper: case-split on the inductive type CausalTetType (two constructors), then norm_num unfolds alphaMin to the concrete rationals $1/3$ and $1/2$ and discharges $0<$ on each. No external lemmas beyond the definition of alphaMin.
why it matters
Positivity of $\alpha_{\min}$ is the bridge from the open half-line $\alpha>\alpha_{\min}(\tau)$ to the strict positivity hypothesis $0<\alpha$ required by edge-positivity lemmas. Downstream, euclideanCausalTet packages the Euclideanized causal tetrahedron as a NonDegenerateTet of the Regge foundation, using lt_trans (alphaMin_pos ty) halpha inside sqEdge_pos. The same pattern appears in the 4d lane (euclideanCausalPent).
Within the module goals this closes the non-degeneracy side of the kinematical Wick rotation: once $\alpha$ sits above the certified threshold, the Euclideanized simplex is non-degenerate and the deficit-angle reality corollary at the physical point $\alpha=1$ is in range. It does not itself touch the Recognition forcing chain (T0–T8), but it is the discrete-gravity substrate on which Lorentzian CDT kinematics is certified.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.