lorentzian_cm4_neg_threeTwo
plain-language theorem explainer
For a Lorentzian (3,2) causal 4-simplex with spatial scale a>0 and timelike parameter α≥0, the 4D Cayley-Menger determinant on the squared-edge tuple is strictly negative. Anyone certifying Lorentzian non-degeneracy of CDT (3,2) pents cites this. The proof rewrites to the closed form −((12α+7)a⁸) and finishes by elementary positivity.
Claim. Let $a>0$ and $\alpha\ge 0$. Equip a causal $(3,2)$ 4-simplex with Lorentzian squared edge lengths (spacelike edges $a^2$, timelike edges $-\alpha a^2$). Then its 4D Cayley-Menger determinant satisfies $\mathrm{cm}_4<0$.
background
This module is the 4D Lorentzian lift of the causal-simplex / Wick machinery in the QG Seven-Gaps campaign (Phase 3a). In Ambjørn–Jurkiewicz–Loll CDT, adjacent spatial slices of equilateral tetrahedra (squared edge $a^2$) are filled by two 4-simplex types. Type $(3,2)$ places three vertices on slice $t$ and two on $t+1$, giving four spacelike and six timelike edges (the time reflection $(2,3)$ shares the same edge multiset).
In the Lorentzian regime, spacelike squared lengths are $a^2$ and timelike squared lengths are $-\alpha a^2$ with $\alpha\ge 0$. The quantity $\mathrm{cm}_4$ is the bordered $6\times 6$ Cayley-Menger determinant for a 4-simplex (via the dimension-parametric cmDetN). Euclidean non-degeneracy is $\mathrm{cm}_4>0$ with all squared edges positive; the Lorentzian side is expected to give strict negativity.
An upstream closed-form evaluation of $\mathrm{cm}_4$ on the Lorentzian $(3,2)$ edge tuple yields exactly $-((12\alpha+7)a^8)$, which is the algebraic input this theorem signs.
proof idea
Term-mode proof in three steps. First rewrite by the closed-form identity that evaluates $\mathrm{cm}_4$ on the Lorentzian $(3,2)$ squared-edge assignment to $-((12\alpha+7)a^8)$. From $a>0$ obtain $a^8>0$ by pow_pos. From $\alpha\ge 0$ obtain $12\alpha+7>0$, hence the product $(12\alpha+7)a^8>0$ by mul_pos. A final linarith turns the rewritten equality into the strict inequality $\mathrm{cm}_4<0$.
why it matters
Closes the Lorentzian half of the cm4-sign ledger for the $(3,2)$ class: Euclidean thresholds give positivity above a critical $\alpha$, and this theorem gives strict negativity on the Lorentzian side for all $\alpha\ge 0$. Downstream, threePent_lorentzian_cm4_neg packages the same certificate for every pent of a three-pent complex, quoting the explicit form $\mathrm{cm}_4=-((12\alpha+7)a^8)<0$ as the per-pent Lorentzian Cayley-Menger certificate.
In the Seven-Gaps Lorentzian-sector lane this is the kinematical check that Wick-rotated $(3,2)$ simplices remain non-degenerate in the CM sense (the 4D analogue of the Regge foundation's non-degenerate tetrahedron criterion). It sits under the D=3 spatial forcing (T8) only indirectly: the ambient CDT setup is 3+1, while the determinant itself is pure 4-simplex linear algebra. No open scaffold remains; the claim is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.