cm4_lorentzian_threeTwo
plain-language theorem explainer
Exact closed form for the bordered Cayley-Menger determinant of a type-(3,2) Lorentzian causal 4-simplex: cm4 equals -((12α+7)a^8). Cited by anyone proving Lorentzian non-degeneracy or Wick-rotation sign flip in the 4D CDT lane. Proof unfolds the parametric 6×6 determinant, substitutes the explicit (3,2) edge matrix, applies a precomputed det identity, and finishes by ring.
Claim. For real $a$ and $\alpha$, the 4-simplex Cayley-Menger determinant on the type-$(3,2)$ Lorentzian squared-edge assignment (spacelike edges $a^2$, timelike edges $-\alpha a^2$) equals $-((12\alpha+7)\,a^8)$.
background
This module is Phase 3a of the QG Seven-Gaps Lorentzian lane: causal (CDT-style) 4-simplex classes in D=4, with Wick rotation as the algebraic continuation α ↦ -α on squared edge lengths. Spatial slices are equilateral tetrahedra of squared edge a²; spacetime between slices is filled by two simplex types.
Type (3,2) places three vertices on slice t and two on t+1, giving four spacelike and six timelike edges (the reflection (2,3) shares the same multiset). In the Lorentzian regime, spacelike squared lengths are a² and timelike ones are -α a² with α>0. The 4-simplex Cayley-Menger determinant cm4 is the bordered 6×6 determinant cmDetN from Geometry.CayleyMengerN; it is homogeneous of degree 4 in the squared distances, so a² scales out as a^8 (the 4D analog of cm3_scaling).
The companion exact evaluation for type (4,1) and the Euclidean thresholds sit in the same file; both feed the strict cm4-negativity statements on the Lorentzian side.
proof idea
Term-mode, four steps. Unfold cm4 to the underlying bordered determinant cmDetN. Rewrite the matrix by the explicit Lorentzian (3,2) edge assignment cmMatrixN_lorentzian_threeTwo. Replace the determinant by the precomputed closed form det_pentMatrix32. Finish with ring, which matches the polynomial -((12α+7)a^8).
why it matters
Supplies the exact Lorentzian (3,2) evaluation needed by lorentzian_cm4_neg_threeTwo, which concludes cm4<0 whenever a>0 and α≥0 (the product (12α+7)a^8 is strictly positive). That negativity is the 4D Lorentzian half of the module's non-degeneracy package: Euclidean side has positive cm4 above an α-threshold; Lorentzian side is strictly negative for both causal classes.
In the broader Recognition framework this is kinematical scaffolding for the gravity Seven-Gaps campaign, not a forcing-chain step. It lifts the already kernel-checked 3D causal-simplex Wick machinery to 4D CDT conventions (Ambjørn-Jurkiewicz-Loll), using the dimension-parametric Cayley-Menger infrastructure. Spatial D=3 (T8) is ambient background; the simplex itself is the 4D spacetime cell. No open sorry remains on this identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.