alphaMin_lt_one
plain-language theorem explainer
For either CDT causal 4-simplex type ((4,1) or (3,2)), the Euclidean non-degeneracy threshold alphaMin is strictly less than 1. Anyone building physical-point witnesses at unit spacing and alpha = 1 cites this. The proof is a two-case numeric evaluation of the closed-form thresholds.
Claim. For every causal 4-simplex type $\mathrm{ty}\in\{(4,1),(3,2)\}$, the Euclidean cm4-positivity threshold satisfies $\alpha_{\min}(\mathrm{ty})<1$.
background
This module is the 4D Lorentzian lift in the QG Seven-Gaps campaign (Phase 3a). Between adjacent spatial slices of equilateral tetrahedra (squared edge $a^2$), spacetime is filled by two CDT 4-simplex classes: type (4,1) with four vertices on slice $t$ and one on $t+1$ (6 spacelike + 4 timelike edges), and type (3,2) with three on $t$ and two on $t+1$ (4 spacelike + 6 timelike). Timelike squared lengths are $-\alpha a^2$ in the Lorentzian regime ($\alpha>0$); Wick rotation continues $\alpha\mapsto -\alpha$.
Non-degeneracy of the Euclideanized simplex is controlled by the Cayley–Menger determinant $\mathrm{cm4}$ (the bordered $6\times 6$ form from CayleyMengerN). The exact threshold $\alpha_{\min}(\mathrm{ty})$ is the unique positive root where $\mathrm{cm4}=0$; the core range theorem states that for $a>0$, $\mathrm{cm4}>0$ iff $\alpha>\alpha_{\min}(\mathrm{ty})$.
The physical calibration point used downstream is unit spacing $a=1$ with $\alpha=1$. That point is admissible only if both thresholds sit strictly below 1.
proof idea
Case-split on the inductive type CausalPentType (constructors fourOne and threeTwo). On each branch, unfold the closed-form definition of alphaMin and discharge the strict inequality by norm_num. No external lemmas beyond the definition of the two numeric thresholds.
why it matters
Feeds the packaged physical witness physicalCausalPent, which builds a non-degenerate Euclidean causal 4-simplex at $(a,\alpha)=(1,1)$ by calling the Euclidean constructor with one_pos and this inequality. The same pattern appears in the 3D precursor CausalSimplexWick.physicalCausalTet via the parallel theorem there.
In the Seven-Gaps Lorentzian-sector lane this closes the kinematical check that the standard CDT physical point lies strictly inside the Euclidean non-degeneracy chamber for both 4-simplex classes, before deficit-angle and dynamics work. It sits under the D=3 spatial forcing (T8) already baked into the CDT slice geometry, and under the Wick map $\alpha\mapsto -\alpha$ that links Lorentzian and Euclidean regimes in this module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.