Gravity Seven Gaps Causal Simplex Wick Is Timelike Two Two Eq Cross Slice

The cross-slice rule

In the causal dynamical triangulations approach to quantum gravity, spacetime is built from flat simplexes glued together, much as a surface can be tiled by triangles. A tetrahedron, the four-vertex simplex in three dimensions, has six edges. The framework assigns each vertex to one of two consecutive time slices, and each edge is then classified by whether its two endpoints lie on the same slice or on different slices. The declaration isTimelike_twoTwo_eq_crossSlice proves, by direct computation over the finite set of edges, that for the tetrahedron type with two vertices on each slice, an edge is timelike exactly when its endpoints belong to different slices. In other words, the classification of an edge as timelike is not an independent assumption; it follows from the slice structure alone.

The proof is a decidable check: there are only six edges and two slices, so the equivalence is verified by evaluating every case. The theorem is part of a larger, machine-checked library of formal theorems. It does not prove anything about the physics of time or about the geometry of the tetrahedron; it only certifies the combinatorial labeling. The declaration is one of a pair, the other covering the tetrahedron type with three vertices on one slice and one on the next. Together they establish that the edge-type assignment used in the Lorentzian sector is consistent with the causal structure of the slices.

The theorem does not claim that the timelike edges have any particular squared length, nor that the tetrahedron is geometrically realizable. Those questions are handled by separate definitions and theorems. The declaration also does not address the action-level continuation of the theory, which remains an open target. What it does establish is a clean combinatorial fact: in the (2,2) tetrahedron, the four edges that cross between slices are precisely the four timelike edges. This fact is what lets the framework define the Wick rotation, the map that flips the sign of timelike squared lengths, as a purely algebraic continuation on the edge data.

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

What this page does not claim

No claim about the geometry or physical length of the timelike edges. No claim about the real-world existence of spacetime tetrahedra. No claim about the action-level Lorentzian continuation, which remains open.

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: