euclideanCausalPent
plain-language theorem explainer
Packages a Euclideanized causal 4-simplex of either CDT type into a non-degenerate pentuple once the squared scale a is positive and the anisotropy alpha exceeds the type-dependent threshold. All ten squared edges are positive and the 4D Cayley-Menger determinant is strictly positive. Downstream code cites it to obtain a concrete NonDegeneratePent witness, including the physical point a=1, alpha=1. The body just wires the two positivity lemmas into the structure fields.
Claim. For either causal 4-simplex type $\mathrm{ty}\in\{(4,1),(3,2)\}$ and real parameters $a,\alpha$ with $0<a$ and $\alpha>\alpha_{\min}(\mathrm{ty})$, the Euclideanized squared-edge 10-tuple is a non-degenerate Euclidean 4-simplex: every squared edge length is positive and the bordered Cayley-Menger determinant $\mathrm{cm}_4$ is strictly positive.
background
This module is the 4D Lorentzian lift in the QG Seven-Gaps campaign (Phase 3a). Spatial slices are equilateral 3-tetrahedra of squared edge $a^2$; spacetime between adjacent slices is filled by two CDT 4-simplex classes: type $(4,1)$ (six spacelike, four timelike edges) and type $(3,2)$ (four spacelike, six timelike). In the Lorentzian regime timelike squared lengths are $-\alpha a^2$ with $\alpha>0$; Wick rotation is the algebraic continuation $\alpha\mapsto -\alpha$.
A NonDegeneratePent is the 4D analogue of the Regge foundation's non-degenerate tetrahedron: a 10-tuple of squared edges that are all positive and whose 4-simplex Cayley-Menger determinant $\mathrm{cm}4$ (the bordered $6\times 6$ determinant from Geometry.CayleyMengerN) is strictly positive. The Euclidean squared-edge map and the exact thresholds $\alpha{\min}(\mathrm{ty})$ are already established in-module; this definition only packages them.
proof idea
Definitional packaging, not a new argument. The squared-edge field is the Euclidean edge map euclideanSqEdges ty a alpha. Positivity of every edge is discharged by euclideanSqEdges_pos, using $0<a$ and $\alpha>0$ via lt_trans through alphaMin_pos. The $\mathrm{cm}4>0$ field is exactly the existing lemma cm4_euclidean_pos on the open range $\alpha>\alpha{\min}(\mathrm{ty})$.
why it matters
Closes the Euclidean non-degeneracy side of the 4D kinematical Wick rotation at the cm4-criterion level: Lorentzian class member in, Euclidean $\mathrm{cm}4>0$ out (embeddability upgrade is classical and left unformalized). The sole immediate consumer is physicalCausalPent, which specializes to the physical point $a=1$, $\alpha=1$ once $\alpha{\min}(\mathrm{ty})<1$ is known. That witness feeds the module status certificate for the 4D Lorentzian lift. In the broader RS gravity lane this is the D=4 CDT counterpart of the kernel-checked 3D causal-simplex Wick machinery, sitting under the forced spatial dimension D=3 of the forcing chain only as ambient geometry, not as a new forcing step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.