lorentzian_cm3_neg_twoTwo
plain-language theorem explainer
For Lorentzian (2,2) CDT tetrahedra with spatial scale a>0 and timelike parameter α≥0, the Cayley–Menger cubic on the squared-edge 6-tuple is strictly negative. Discrete-gravity and Regge analysts cite this to certify that the Lorentzian edge assignment is non-Euclidean in sign. Proof: rewrite via the closed-form (2,2) formula, then positivity of a⁶ and (2α+1)a⁶ plus linarith.
Claim. Let $a>0$ and $\alpha\ge 0$. Form the Lorentzian squared-edge 6-tuple of a causal $(2,2)$ tetrahedron (two vertices on each adjacent spatial slice; spacelike edges $a^2$, timelike edges $-\alpha a^2$). Then its Cayley–Menger cubic satisfies $\mathrm{CM}_3<0$.
background
This module is the Lorentzian-sector lane of the QG Seven-Gaps campaign in $D=3$ CDT (Ambjørn–Jurkiewicz–Loll). Spatial slices are equilateral triangulations with squared edge $a^2$. Between slices, two tetrahedron types fill spacetime: $(3,1)$ (three vertices on $t$, one on $t+1$) and $(2,2)$ (two on each slice). Spacelike edges keep $a^2$; timelike edges carry $-\alpha a^2$ with $\alpha>0$ in the Lorentzian regime. Wick rotation is the algebraic continuation $\alpha\mapsto -\alpha$ on that class.
The Cayley–Menger cubic $\mathrm{CM}_3$ is the standard 4-point polynomial in the six squared edge lengths (from Geometry.CayleyMengerPolynomial); its sign tracks oriented volume-squared and Euclidean non-degeneracy. The map lorentzianSqEdges builds the length-squared 6-tuple for a chosen causal type. Edge indexing is fixed: vertices $0,1,2,3$; for $(2,2)$, ${0,1}$ lie on slice $t$ and ${2,3}$ on $t+1$ (two spacelike + four timelike edges).
The companion closed form cm3_lorentzian_twoTwo evaluates $\mathrm{CM}_3$ on that tuple; the present theorem only needs its sign under $a>0$, $\alpha\ge 0$.
proof idea
Term/tactic hybrid, four steps. Rewrite the goal by the closed-form identity cm3_lorentzian_twoTwo, which reduces $\mathrm{CM}_3$ on the Lorentzian $(2,2)$ edges to an explicit rational expression in $a$ and $\alpha$. From $a>0$ obtain $a^6>0$ by pow_pos. From $\alpha\ge 0$ get $2\alpha+1>0$, hence $(2\alpha+1)a^6>0$ by mul_pos. Finish with linarith, which reads the rewritten formula as strictly negative once that positive factor is in hand. No case split on type and no numeric approximation.
why it matters
Certifies the Lorentzian sign of volume-squared for the $(2,2)$ CDT class before any Wick flip. The module’s next block packages Euclideanized non-degeneracy (NonDegenerateTet: all squared edges positive and $\mathrm{CM}3>0$) on the exact range $\alpha>\alpha{\min}(\mathrm{type})$, and a deficit-angle reality corollary at the physical point $\alpha=1$. This lemma is the Lorentzian counterpart that makes the sign flip under $\alpha\mapsto -\alpha$ meaningful: Lorentzian $\mathrm{CM}_3<0$ versus Euclideanized $\mathrm{CM}_3>0$.
It sits in the discrete-gravity stack that already forces $D=3$ (forcing chain T8) and the eight-tick octave (T7), and it supplies the missing Lorentzian edge of prior Euclidean Regge/Cayley–Menger work. No downstream uses are wired yet (used_by empty); the natural consumers are the packaged Wick composite and any later Lorentzian Regge action or causal-dynamical path-integral bounds in the Seven-Gaps list.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.