Gravity Seven Gaps Causal Simplex Wick

The Wick rotation, made discrete

In physics, a Wick rotation is a mathematical trick: replace time with imaginary time to turn the equations of a relativistic theory into those of an ordinary Euclidean one. It is a standard tool in quantum field theory, where it turns oscillating path integrals into well-behaved ones. The module gravity seven gaps causal simplex wick applies this idea to a discrete model of spacetime, where space and time are built from simple building blocks called simplices (the generalization of a triangle to higher dimensions).

The model is the causal dynamical triangulations (CDT) approach, developed by Jan Ambjørn, Jerzy Jurkiewicz, and Renate Loll. Spacetime is approximated by a stack of two-dimensional spatial slices, each a triangulated surface of equilateral triangles. The space between two consecutive slices is filled with two types of tetrahedra: type (3,1), with three vertices on one slice and one on the next, and type (2,2), with two vertices on each. In the Lorentzian regime, spacelike edges have squared length a², while timelike edges have squared length -αa² with α > 0. The Wick rotation here is an explicit map that flips the sign of the timelike squared lengths, turning a Lorentzian tetrahedron into a Euclidean one.

The central result is that this map is an involution: applying it twice returns the original configuration. It also proves that the map acts on the causal class as the algebraic continuation α ↦ -α, meaning the Wick rotation is not just a formal operation but a genuine transformation of the theory's parameter. A non-degeneracy theorem then shows that the Euclideanized simplices are non-degenerate, meaning they have non-zero volume, exactly when α > 1/3 for type (3,1) and α > 1/2 for type (2,2). Both types are simultaneously non-degenerate exactly for α > 1/2, the standard 3d CDT Euclidean-regime bound. On the Lorentzian side, the Cayley-Menger polynomial, which measures volume, is always negative, so the Lorentzian tuples are never Euclidean-realizable and the Wick rotation is genuinely required.

Finally, at the physical point α = 1, the Euclideanized simplices coincide with the regular tetrahedron, and all dihedral angles are real and equal to arccos(1/3). This is a concrete, checkable consequence. The module is part of the Seven-Gaps campaign, the first certified Lorentzian layer of the discrete gravity program, where all prior results were Euclidean. The action-level Lorentzian continuation, involving complex dihedral angles and the sinh-action sector, remains open. The module explicitly flags this as an open problem in its status structure.

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

/-- THEOREM: combining the two, the Wick map acts on the causal class as
the continuation `alpha ↦ -alpha`. -/
theorem wick_eq_continuation (ty : CausalTetType) (a alpha : ℝ) :
    wick ty (lorentzianSqEdges ty a alpha) = lorentzianSqEdges ty a (-alpha) :=
  (wick_lorentzian ty a alpha).trans (lorentzian_continuation ty a alpha).symm

/-- THEOREM (core, exact range): for `0 < a`, the Euclideanized causal
tetrahedron is non-degenerate (`cm3 > 0`, equivalently positive squared
volume) if and only if `alpha > alphaMin ty`.  The threshold is exact in
both directions. -/
theorem cm3_euclidean_pos_iff (ty : CausalTetType) (a alpha : ℝ)
    (ha : 0 < a) :
    0 < cm3 (euclideanSqEdges ty a alpha) ↔ alphaMin ty < alpha := by
  have h6 : 0 < a ^ 6 := pow_pos ha 6
  cases ty
  · rw [cm3_euclidean_threeOne, alphaMin_threeOne]
    constructor
    · intro h
      by_contra hle
      push_neg at hle
      have hprod : 0 ≤ (1 - 3 * alpha) * a ^ 6 :=
        mul_nonneg (by linarith) h6.le
      linarith
    · intro h
      have hprod : 0 < (3 * alpha - 1) * a ^ 6 :=
        mul_pos (by linarith) h6
      linarith
  · rw [cm3_euclidean_twoTwo, alphaMin_twoTwo]
    constructor
    · intro h
      by_contra hle
      push_neg at hle
      have hprod : 0 ≤ (1 - 2 * alpha) * a ^ 6 :=
        mul_nonneg (by linarith) h6.le
      linarith
    · intro h
      have hprod : 0 < (2 * alpha - 1) * a ^ 6 :=
        mul_pos (by linarith) h6
      linarith

theorem alphaMin_lt_one (ty : CausalTetType) : alphaMin ty < 1 := by
  cases ty <;> norm_num [alphaMin]

/-- THEOREM: the Euclidean dihedral angle at every edge of the physical-point
causal tetrahedron is `arccos (1/3)`, hence strictly inside `(0, π)`:
deficit angles at all edges are real and well-defined. -/
theorem dihedralAngle3_physical (ty : CausalTetType) (e : Fin 6) :
    dihedralAngle3 (physicalCausalTet ty) e = Real.arccos (1 / 3) :=
  congrArg Real.arccos (dihedralCos3Sq_alpha_one ty e)

What this page does not claim

This module does not prove the action-level Lorentzian continuation with complex dihedral angles. It does not provide a physical interpretation of the parameter α beyond its role in the edge length assignments. It does not establish that this discrete model is a correct description of quantum gravity.

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/CausalSimplexWick.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: