Gravity Seven Gaps Causal Simplex4 D Causal Simplex4 Dstatus Flags

The status record

A causal simplex is the basic building block of spacetime in a discrete approach to quantum gravity called causal dynamical triangulations. In four dimensions, spacetime is assembled from two types of four-simplex, the four-dimensional analogue of a triangle. The first type has four vertices on one spatial slice and one on the next; the second has three on one slice and two on the next. Each type is defined by which of its ten edges are spacelike and which are timelike. The machine-checked library of formal theorems in the Recognition Science framework contains a record called causalSimplex4DStatus, a documentation structure that stores four boolean flags summarizing what has been established for these objects.

The first flag records that the two causal four-simplex classes are defined, with their edge types verified combinatorially. The second flag records that the exact thresholds for non-degeneracy are certified: the first simplex type remains non-degenerate for a parameter alpha greater than 3/8, and the second for alpha greater than 7/12, so both are simultaneously valid only for alpha greater than 7/12. The third flag records that the Lorentzian side, where timelike edges carry negative squared length, is proved to have a strictly negative Cayley-Menger determinant, meaning the simplex cannot be realized in Euclidean space. The fourth flag is set to false, marking that the action-level continuation, the next stage of the calculation, remains open. This record is a documentation device, not a theorem; it summarizes the state of the formal development.

The record itself makes no mathematical claim. It is a hand-set collection of booleans that points to the actual theorems. The theorems behind the flags are proved with zero axioms beyond the standard three. The Wick rotation, which flips the sign of timelike squared lengths, is proved to be an involution and to act as the continuation alpha to negative alpha. The Cayley-Menger determinant is evaluated exactly for both causal classes, giving the thresholds above. At the physical point alpha equals one, both types reduce to the regular four-simplex with determinant 5 times a to the eighth power.

What the record does not claim is as important as what it does. The classical equivalence between a positive Cayley-Menger determinant and embeddability in four-dimensional Euclidean space is not formalized in this library; only the sign fact is proved. The action-level Lorentzian continuation, involving complex dihedral angles at timelike hinges and the boost sector of the Regge action, is deliberately not attempted and remains open. The record is a status summary for the geometric layer, not a claim about the full physical theory.

/-- The two causal 4-simplex types of 4d CDT between adjacent slices.
`fourOne` has four vertices on slice `t` and one on slice `t+1` (its time
reflection (1,4) has the same edge data); `threeTwo` has three vertices on
slice `t` and two on slice `t+1` (reflection (2,3) likewise). -/
inductive CausalPentType
  | fourOne
  | threeTwo

/-- 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 alphaMin_fourOne : alphaMin CausalPentType.fourOne = 3 / 8 := rfl

theorem alphaMin_threeTwo : alphaMin CausalPentType.threeTwo = 7 / 12 := rfl

/-- 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: 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: combining the two, the Wick map acts on the causal class as
the continuation `alpha ↦ -alpha`. -/
theorem wick_eq_continuation (ty : CausalPentType) (a alpha : ℝ) :
    wick ty (lorentzianSqEdges ty a alpha) = lorentzianSqEdges ty a (-alpha) :=
  (wick_lorentzian ty a alpha).trans (lorentzian_continuation ty a alpha).symm

What this page does not claim

The record does not prove that a positive Cayley-Menger determinant implies embeddability in four-dimensional Euclidean space; that equivalence is not formalized in this library. The record does not claim that the action-level Lorentzian continuation is complete; that remains open. The record does not assert that the causal four-simplex classes are the only possible building blocks for four-dimensional spacetime.

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: