Gravity Seven Gaps Causal Simplex Wick Lorentzian Sector Status Flags

Status flags

A status flag is a simple yes or no record of what has been accomplished. The declaration lorentzianSectorStatus sets four such flags for a specific piece of work in discrete gravity, the study of spacetime built from flat triangular and tetrahedral pieces. The first flag says the causal tetrahedron classes are defined: the two basic building blocks, one with three vertices on an earlier time slice and one on a later slice, the other with two vertices on each, have been encoded as formal objects. The second flag says the Wick rotation is certified on those classes: the map that flips the sign of the squared length of timelike edges, turning a Lorentzian geometry into a Euclidean one, has been proved to be an involution, meaning applying it twice returns the original configuration. The third flag says non-degeneracy is proved for the Euclideanized simplices, meaning the tetrahedra have nonzero volume exactly when a parameter alpha exceeds a threshold, 1/3 for one type and 1/2 for the other. The fourth flag says the action-level Lorentzian continuation is open: the complex dihedral angles and the sinh-action sector have not been attempted.

These flags are not a theory of quantum gravity. They are a status report on a formal library, a machine-checked collection of theorems and definitions. The first three flags being true means that specific statements have been proved with no gaps in their logical derivation. The fourth flag being true means the opposite: the action-level continuation remains a target for future work, not an established result. The flags do not claim that the causal tetrahedron classes are the correct description of physical spacetime, nor that the Wick rotation as defined here matches the full procedure used in continuum physics. They only certify that within this formal system, certain combinatorial and algebraic facts hold.

What the flags do not claim is as important as what they do. They do not claim that the Lorentzian sector of discrete gravity is complete or that the open action-level continuation is impossible. They do not claim that the thresholds 1/3 and 1/2 are physically meaningful bounds on a coupling constant; they are conditions for the Euclideanized tetrahedra to have nonzero volume. They do not claim that the Wick rotation is a physical process, only that it is a well-defined algebraic map on squared edge lengths. The flags are a precise inventory: what is proved, what is defined, and what remains open, nothing more.

/-- The two causal tetrahedron types of 3d CDT between adjacent slices.
`threeOne` has three vertices on slice `t` and one on slice `t+1` (its time
reflection (1,3) has the same edge data); `twoTwo` has two vertices on each
slice. -/
inductive CausalTetType
  | threeOne
  | twoTwo

/-- 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 (composite): the Wick image of the Lorentzian causal tuple is
non-degenerate on the exact range.  This is the certified kinematical Wick
rotation: Lorentzian class member in, `NonDegenerateTet`-certified Euclidean
tetrahedron out (realizability in the cm3-criterion sense above). -/
theorem wick_lorentzian_nondegenerate (ty : CausalTetType) (a alpha : ℝ)
    (ha : 0 < a) (halpha : alphaMin ty < alpha) :
    0 < cm3 (wick ty (lorentzianSqEdges ty a alpha)) := by
  rw [wick_lorentzian]
  exact cm3_euclidean_pos ty a alpha ha halpha

What this page does not claim

The flags do not claim the causal tetrahedron classes are the correct physical description of spacetime. The flags do not claim the thresholds 1/3 and 1/2 are physically meaningful bounds on a coupling constant. The flags do not claim the action-level Lorentzian continuation is impossible, only that it is not yet proved.

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: