alphaMin_pos
plain-language theorem explainer
For both CDT causal 4-simplex types, the Euclidean non-degeneracy threshold α_min is strictly positive: 3/8 for (4,1) and 7/12 for (3,2). Anyone packaging a NonDegeneratePent from a Euclideanized causal simplex cites this to turn α > α_min into 0 < α. The proof is a two-case split with a numerical check of the defining constants.
Claim. Let $\mathrm{ty}$ be either causal 4-simplex type of 4d CDT: $(4,1)$ or $(3,2)$. Write $\alpha_{\min}(\mathrm{ty})$ for the exact Euclidean non-degeneracy threshold of that type ($3/8$ and $7/12$ respectively). Then $0 < \alpha_{\min}(\mathrm{ty})$.
background
This module is the 4D Lorentzian lift of the 3D causal-simplex Wick machinery (QG Seven-Gaps, Phase 3a). Between adjacent spatial slices of equilateral tetrahedra with squared edge length $a^2$, spacetime is filled by two CDT 4-simplex classes: type $(4,1)$ (four vertices on slice $t$, one on $t+1$; six spacelike and four timelike edges) and type $(3,2)$ (three on $t$, two on $t+1$; four spacelike and six timelike). Timelike squared lengths are $-\alpha a^2$ in the Lorentzian regime with $\alpha > 0$; Wick rotation continues $\alpha \mapsto -\alpha$.
The sibling definition alphaMin records the exact cm4-positivity thresholds: $\alpha_{\min}(4,1) = 3/8$ and $\alpha_{\min}(3,2) = 7/12$. The 3D analogue in CausalSimplexWick uses $1/3$ and $1/2$ for the tetrahedron types and has the same positivity lemma. Downstream packaging of a Euclidean nondegenerate 4-simplex needs $0 < \alpha$ as an intermediate inequality whenever $\alpha > \alpha_{\min}$.
proof idea
One-line wrapper: case-split on the inductive type CausalPentType (two constructors), then norm_num against the definition of alphaMin, which is the literal rationals $3/8$ and $7/12$. Identical shape to the 3D alphaMin_pos for tetrahedra.
why it matters
Feeds the packaged witness euclideanCausalPent: on $\alpha > \alpha_{\min}(\mathrm{ty})$ with $a > 0$, the Euclideanized causal 4-simplex is a NonDegeneratePent (all squared edges positive and cm4 $> 0$). The positivity proof of squared edges applies lt_trans (alphaMin_pos ty) halpha to obtain $0 < \alpha$ from the strict threshold inequality. The same pattern appears in the 3D euclideanCausalTet. Within the Seven-Gaps Lorentzian lane this is the elementary positivity hinge that lets the exact cm4 non-degeneracy thresholds become usable hypotheses for Euclideanized causal simplices, before the Wick involution and Lorentzian-side cm4 negativity are applied.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.