Gravity Seven Gaps Causal Simplex4 D Cm Matrix N Lorentzian Four One

The Lorentzian 4-simplex

In causal dynamical triangulations (a lattice approach to quantum gravity), spacetime is built from flat 4-simplexes, the four-dimensional analog of triangles. Each simplex has ten edges, and a classical formula called the Cayley-Menger determinant computes the square of its volume from those edge lengths. The declaration cmMatrixN_lorentzian_fourOne is a theorem about the (4,1) simplex type, which has four vertices on one spatial slice and one on the next. It proves that when the timelike edges carry a negative squared length, as they do in the Lorentzian signature of special relativity, the Cayley-Menger determinant is strictly negative for any positive time parameter.

This matters because a negative volume-squared means the simplex cannot be embedded in ordinary four-dimensional Euclidean space. The classical reading, not formalized in this library, is that such a simplex is not geometrically realizable. The framework's library proves the sign fact exactly: for the (4,1) type, the determinant equals -(8*alpha + 3) * a^8, where a is the spatial edge length and alpha the time parameter. At alpha = 1, the physical point, both simplex types reduce to the regular 4-simplex with determinant 5 * a^8.

The theorem pairs with a second one for the (3,2) type, which has three vertices on one slice and two on the next, giving -(12*alpha + 7) * a^8. Together they certify that both Lorentzian building blocks are never Euclidean-realizable. This is why the framework's library defines a Wick rotation, a map that flips the sign of timelike squared lengths, turning the Lorentzian simplex into a Euclidean one. The library proves this map is an involution, meaning applying it twice returns the original, and that it acts as the algebraic continuation alpha to -alpha.

After the rotation, the Euclideanized simplexes become non-degenerate exactly when alpha exceeds a threshold: 3/8 for the (4,1) type and 7/12 for the (3,2) type. Both are simultaneously valid above 7/12, the standard bound in 4D causal dynamical triangulations. The library proves these thresholds are exact, with degeneracy precisely at the boundary. What it does not prove is the classical equivalence that a positive determinant means embeddability in Euclidean 4-space; that realizability theorem remains open for four dimensions, though a three-dimensional analog exists. The action-level continuation, involving complex angles and the full Regge action, is also deliberately not attempted.

/-- THEOREM: type (4,1) Lorentzian Cayley-Menger determinant,
`cm4 = -((8*alpha + 3) * a^8)`: strictly negative for `alpha ≥ 0`, `0 < a`
(see `lorentzian_cm4_neg_fourOne`). -/
theorem cm4_lorentzian_fourOne (a alpha : ℝ) :
    cm4 (lorentzianSqEdges CausalPentType.fourOne a alpha)
      = -((8 * alpha + 3) * a ^ 8) := by
  unfold cm4 cmDetN
  rw [cmMatrixN_lorentzian_fourOne, det_pentMatrix41]
  ring

/-- THEOREM: the Wick map is involutive (Mathlib `Function.Involutive`
packaging of `wick_wick`). -/
theorem wick_involutive (ty : CausalPentType) :
    Function.Involutive (wick ty) :=
  fun x => wick_wick ty x

/-- THEOREM (core, exact range): for `0 < a`, the Euclideanized causal
4-simplex satisfies the CM positivity criterion `cm4 > 0` if and only if
`alpha > alphaMin ty`.  The threshold is exact in both directions.
Reading note: `cm4 > 0` is `9216 * simplexVolumeSqN > 0` (proved above);
its classical equivalence to embeddability in R^4 is not formalized in
this repo for n = 4 (3D analog: `Geometry/TetrahedronRealization.lean`). -/
theorem cm4_euclidean_pos_iff (ty : CausalPentType) (a alpha : ℝ)
    (ha : 0 < a) :
    0 < cm4 (euclideanSqEdges ty a alpha) ↔ alphaMin ty < alpha := by
  have h8 : 0 < a ^ 8 := pow_pos ha 8
  cases ty
  · rw [cm4_euclidean_fourOne, alphaMin_fourOne]
    constructor
    · intro h
      by_contra hle
      push_neg at hle
      have hprod : 0 ≤ (3 - 8 * alpha) * a ^ 8 :=
        mul_nonneg (by linarith) h8.le
      linarith
    · intro h
      have hprod : 0 < (8 * alpha - 3) * a ^ 8 :=
        mul_pos (by linarith) h8
      linarith
  · rw [cm4_euclidean_threeTwo, alphaMin_threeTwo]
    constructor
    · intro h
      by_contra hle
      push_neg at hle
      have hprod : 0 ≤ (7 - 12 * alpha) * a ^ 8 :=
        mul_nonneg (by linarith) h8.le
      linarith
    · intro h
      have hprod : 0 < (12 * alpha - 7) * a ^ 8 :=
        mul_pos (by linarith) h8
      linarith

/-- THEOREM (core, exact range): for `0 < a`, the Euclideanized causal
4-simplex satisfies the CM positivity criterion `cm4 > 0` if and only if
`alpha > alphaMin ty`.  The threshold is exact in both directions.
Reading note: `cm4 > 0` is `9216 * simplexVolumeSqN > 0` (proved above);
its classical equivalence to embeddability in R^4 is not formalized in
this repo for n = 4 (3D analog: `Geometry/TetrahedronRealization.lean`). -/
theorem cm4_euclidean_pos_iff (ty : CausalPentType) (a alpha : ℝ)
    (ha : 0 < a) :
    0 < cm4 (euclideanSqEdges ty a alpha) ↔ alphaMin ty < alpha := by
  have h8 : 0 < a ^ 8 := pow_pos ha 8
  cases ty
  · rw [cm4_euclidean_fourOne, alphaMin_fourOne]
    constructor
    · intro h
      by_contra hle
      push_neg at hle
      have hprod : 0 ≤ (3 - 8 * alpha) * a ^ 8 :=
        mul_nonneg (by linarith) h8.le
      linarith
    · intro h
      have hprod : 0 < (8 * alpha - 3) * a ^ 8 :=
        mul_pos (by linarith) h8
      linarith
  · rw [cm4_euclidean_threeTwo, alphaMin_threeTwo]
    constructor
    · intro h
      by_contra hle
      push_neg at hle
      have hprod : 0 ≤ (7 - 12 * alpha) * a ^ 8 :=
        mul_nonneg (by linarith) h8.le
      linarith
    · intro h
      have hprod : 0 < (12 * alpha - 7) * a ^ 8 :=
        mul_pos (by linarith) h8
      linarith

What this page does not claim

The classical equivalence between a positive Cayley-Menger determinant and embeddability in Euclidean 4-space is not formalized for n = 4. The action-level Lorentzian continuation in 4D, involving complex dihedral angles and the boost sector, is not attempted here. No claim is made that a negative determinant alone proves non-realizability without the classical geometric reading.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Gravity/SevenGaps/CausalSimplex4D.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: