Gravity Seven Gaps Causal Simplex Wick Is Timelike Three One Eq Cross Slice

The timelike edge rule

In the discrete approach to quantum gravity called causal dynamical triangulations, spacetime is built from flat simplexes glued together along faces. The simplest building block in three dimensions is a tetrahedron, and the simplest way to make it causal is to stack its four vertices on two successive slices of space. One type, called (3,1), places three vertices on the earlier slice and one on the later slice. The other, (2,2), places two vertices on each slice. The question is which of the six edges of such a tetrahedron should count as timelike, meaning that a signal could travel along it from one slice to the other, and which should count as spacelike, lying entirely within a single slice.

The declaration isTimelike_threeOne_eq_crossSlice settles the question for the (3,1) tetrahedron by a direct combinatorial check. It proves that an edge is timelike if and only if its two endpoints lie on different slices. The proof is exhaustive: the machine-checked library of formal theorems enumerates all six edges, compares the slice assignment of each endpoint, and verifies the equality in every case. The same theorem holds for the (2,2) type, where four of the six edges cross between slices. This is a definitional encoding of the standard convention in the field, not a physical discovery: the library chooses to call an edge timelike precisely when it crosses a slice boundary, and then verifies that this choice is consistent across all edges.

The result matters because it makes the geometry of the causal simplex fully explicit. With the edge types fixed, the library goes on to define the squared lengths: spacelike edges carry length a², timelike edges carry length −αa² with α > 0 in the Lorentzian regime. A Wick rotation then flips the sign of the timelike squared lengths, turning the Lorentzian tetrahedron into a Euclidean one. The rotation is proved to be an involution, meaning applying it twice returns the original edge lengths, and it acts on the causal class as the algebraic continuation α ↦ −α. This is the kinematical bridge that lets the framework move between the physical Lorentzian picture and the computationally friendlier Euclidean one.

What the declaration does not claim is just as important. It does not assert that these edge types are forced by physics; they are a modeling choice, the standard one in causal dynamical triangulations. It does not prove anything about the action, the quantity that weights each spacetime history in the path integral. The action-level Lorentzian continuation, involving complex dihedral angles and boost-angle assignments at timelike hinges, is explicitly left open. The theorem is a piece of combinatorial bookkeeping, certified by exhaustive check, that pins down the kinematics of a single tetrahedron. It is the first certified step in a longer campaign to build a Lorentzian sector for the discrete gravity program, not the whole building.

/-- THEOREM (by `decide`): for type (3,1), an edge is timelike iff its two
endpoints (via the repo edge convention `edgeVertices`) lie on different
slices.  This verifies the edge-type table against the slice structure. -/
theorem isTimelike_threeOne_eq_crossSlice :
    ∀ e : Fin 6,
      isTimelike CausalTetType.threeOne e
        = (sliceOf CausalTetType.threeOne (edgeVertices e).1
            != sliceOf CausalTetType.threeOne (edgeVertices e).2) := by
  decide

/-- THEOREM (by `decide`): same cross-slice verification for type (2,2). -/
theorem isTimelike_twoTwo_eq_crossSlice :
    ∀ e : Fin 6,
      isTimelike CausalTetType.twoTwo e
        = (sliceOf CausalTetType.twoTwo (edgeVertices e).1
            != sliceOf CausalTetType.twoTwo (edgeVertices e).2) := by
  decide

/-- 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

What this page does not claim

The edge-type assignment is a modeling choice, not a consequence of physical law. The declaration does not prove anything about the action or the path integral weights. The Lorentzian action continuation is open, not established.

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: