alphaMin
plain-language theorem explainer
Exact Euclidean non-degeneracy thresholds for the two CDT 4-simplex classes: 3/8 on the (4,1) type and 7/12 on the (3,2) type. Anyone citing the cm4-positivity criterion, degeneracy-at-threshold, or the 4D Wick lane will hit this constant. It is a pure two-branch definition, the 4D lift of the 3D CausalSimplexWick thresholds.
Claim. For each causal 4-simplex type $\tau$, the Euclidean non-degeneracy threshold $\alpha_{\min}(\tau)$ equals $3/8$ when $\tau$ is the $(4,1)$ class and $7/12$ when $\tau$ is the $(3,2)$ class.
background
In 4d CDT (Ambjørn–Jurkiewicz–Loll), spacetime between adjacent spatial slices is filled by two 4-simplex types. Type $(4,1)$ has four vertices on slice $t$ and one on $t+1$ (six spacelike, four timelike edges); type $(3,2)$ has three on $t$ and two on $t+1$ (four spacelike, six timelike). Spacelike squared lengths are $a^2$; timelike squared lengths are $-\alpha a^2$ in the Lorentzian regime ($\alpha>0$).
The module evaluates the bordered Cayley–Menger determinant $\mathrm{cm}_4$ on the Euclideanized edge data (Wick: $\alpha\mapsto -\alpha$). Non-degeneracy is the strict positivity $\mathrm{cm}_4>0$. The 3D precursor in CausalSimplexWick used thresholds $1/3$ and $1/2$ for the tetrahedron types; this definition supplies the matching 4D constants.
proof idea
Definition by cases on the inductive type of causal 4-simplex classes: the $(4,1)$ branch returns the rational $3/8$, the $(3,2)$ branch returns $7/12$. No proof body; companion rfl lemmas pin each value.
why it matters
Anchors the exact Euclidean range for both causal classes: $\mathrm{cm}4>0$ iff $\alpha>\alpha{\min}(\tau)$, with $\mathrm{cm}_4=0$ exactly at threshold and strict negativity on the Lorentzian side. Downstream lemmas (alphaMin_pos, alphaMin_lt_one, cm4_euclidean_pos_iff, cm4_euclidean_degenerate_at_min) and the campaign ledger anchor all read this constant. It is the 4D counterpart of the 3D Wick thresholds and closes Phase 3a item 4 of the QG Seven-Gaps Lorentzian lane (kinematical Wick rotation in $D=4$).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.