Gravity Seven Gaps Causal Simplex4 D Wick Lorentzian Nondegenerate

The Wick rotation in four dimensions

In the framework of causal dynamical triangulations, spacetime is built from four-dimensional simplexes, the simplest possible building blocks with five vertices. Each simplex has ten edges, and each edge is either spacelike, with squared length a², or timelike, with squared length −αa² in the Lorentzian regime where α > 0. The two allowed types are the (4,1) simplex, with four vertices on one time slice and one on the next, and the (3,2) simplex, with three on one slice and two on the next.

The Wick rotation is the map that flips the sign of every timelike squared edge length, turning a Lorentzian simplex into a Euclidean one. The declaration wick_lorentzian_nondegenerate proves two things about this map. First, it is an involution: applying it twice returns the original simplex, which means the rotation is reversible and consistent. Second, on the Euclidean side, the Cayley-Menger determinant cm4, a formula that measures whether a set of edge lengths can form a genuine shape in four-dimensional space, is positive exactly when α exceeds a threshold: 3/8 for the (4,1) type and 7/12 for the (3,2) type. At the boundary the determinant is zero, meaning the simplex is degenerate, collapsed flat.

On the Lorentzian side, the same determinant is strictly negative for all α ≥ 0. This is the key result: a Lorentzian simplex, with its negative squared timelike edges, can never satisfy the Euclidean condition for being a realizable shape. The Wick rotation is therefore not an optional convenience but a necessary step to reach a Euclidean geometry where the standard tools of geometry apply. At the physical point α = 1, both types reduce to the regular four-simplex, with cm4 = 5a⁸, matching the classical volume formula.

The proof is machine-checked, meaning every theorem in this file is verified with no gaps, no admitted assumptions, and no new axioms. The definitions of the simplex types, the edge classifications, and the Wick map itself are chosen conventions, not derived results. What is proved is the sign of the determinant and the involution property, not the physical interpretation that a negative determinant means the simplex cannot exist in Euclidean space.

/-- 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: 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: type (3,2) Lorentzian Cayley-Menger determinant,
`cm4 = -((12*alpha + 7) * a^8)`. -/
theorem cm4_lorentzian_threeTwo (a alpha : ℝ) :
    cm4 (lorentzianSqEdges CausalPentType.threeTwo a alpha)
      = -((12 * alpha + 7) * a ^ 8) := by
  unfold cm4 cmDetN
  rw [cmMatrixN_lorentzian_threeTwo, det_pentMatrix32]
  ring

/-- THEOREM (sanity anchor): the regular unit 4-simplex has `cm4 = 5`
(classical: `V = sqrt 5 / 96`, so `9216 V^2 = 5`). -/
theorem cm4_regular_unit : cm4 (fun _ => (1 : ℝ)) = 5 := by
  rw [← euclideanSqEdges_alpha_one CausalPentType.fourOne,
    cm4_euclidean_fourOne]
  norm_num

What this page does not claim

This does not claim that a negative Cayley-Menger determinant proves a simplex cannot exist in Euclidean space, since that equivalence is not formalized for four dimensions. This does not claim to have derived the action-level Wick rotation, which remains an open target. This does not claim that the definitions of the simplex types are derived rather than chosen conventions.

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: