alphaMin_fourOne

In 4d causal dynamical triangulations (Ambjørn–Jurkiewicz–Loll), spacetime between adjacent spatial slices is filled by two 4-simplex classes. Type $(4,1)$ places four vertices on slice $t$ and one on $t+1$ (six spacelike edges of squared length $a^2$, four timelike edges of squared length $-\alpha a^2$ in the Lorentzian regime). Type $(3,2)$ is the complementary split.

The module lifts the 3d causal-simplex Wick machinery to four dimensions and evaluates the Cayley–Menger determinant cm4 (the bordered $6\times 6$ determinant from Geometry.CayleyMengerN) on both classes after Euclideanization. Non-degeneracy is controlled by a type-dependent threshold function: on $(4,1)$ it is $3/8$, on $(3,2)$ it is $7/12$. The 3d analog used thresholds $1/3$ and $1/2$ for the tetrahedron types.

This declaration simply records the $(4,1)$ value as a named equality so downstream positivity and degeneracy theorems can rewrite by it.

One-line reflexivity. The definition of the threshold function sends the fourOne constructor to the literal rational $3/8$, so rfl closes the equality immediately. No lemmas are applied.

Parent theorems rewrite through this equality. Degeneracy at threshold (cm4_euclidean_degenerate_at_min) substitutes $3/8$ then evaluates cm4 to zero by norm_num. The core range theorem (cm4_euclidean_pos_iff) rewrites the positivity criterion to $\alpha > 3/8$ on the $(4,1)$ branch. The joint Euclidean-regime bound (cm4_euclidean_pos_joint) uses it to show both types are simultaneously non-degenerate precisely when $\alpha > 7/12$, the standard 4d CDT Euclidean window.

In the QG Seven-Gaps Lorentzian-sector campaign this pins the exact kinematical threshold for the dominant $(4,1)$ building block before Wick continuation $\alpha\mapsto -\alpha$ is applied. It is the 4d counterpart of the 3d thresholds $1/3$ and $1/2$.