Encyclopedia Gravity Gravity Seven Gaps Causal Simplex4 D

ARTICLE 5 claims 5 theorems

Gravity Seven Gaps Causal Simplex4 D

A machine-checked module certifies the exact geometry of the two building blocks of four-dimensional causal spacetime, and proves when each one is real.

Verify this page

The 4-simplex bridge

In the framework's account of quantum gravity, spacetime is not a smooth fabric but a stack of discrete spatial slices, each a triangulated three-dimensional manifold. The module in question, a file in the framework's machine-checked library of formal theorems, studies the two possible four-dimensional simplexes that can connect one slice to the next. A 4-simplex is the four-dimensional analogue of a triangle: it has five vertices, ten edges, and is the simplest shape that fills a four-dimensional volume. The two types are named (4,1) and (3,2), referring to how many of their five vertices lie on the earlier slice versus the later one.

The module proves exact facts about these shapes. For the (4,1) type, four vertices sit on the earlier slice and one on the later; it has six spacelike edges (lying within a slice) and four timelike edges (pointing between slices). The (3,2) type has the reverse balance: three vertices on the earlier slice, two on the later, four spacelike and six timelike edges. These counts are proved by exhaustive computation over the ten edges, a combinatorial fact that any reader can verify by hand from the slice assignments. The timelike edges carry a squared length of -alpha times a^2, where alpha is a positive parameter and a is the common spacelike edge length; this sign convention is what marks them as timelike.

The central result is a Wick rotation, a mathematical operation that turns a Lorentzian (spacetime) geometry into a Euclidean (spatial-only) one by flipping the sign of the timelike squared lengths. The module defines this map on the ten edge lengths and proves it is an involution: applying it twice returns the original tuple. It also proves that on the causal classes, the map acts exactly as the algebraic continuation alpha maps to -alpha. This is the precise sense in which the Lorentzian and Euclidean regimes are connected: not by a physical process, but by a formal sign flip that the framework's library certifies.

For each type, the module evaluates the Cayley-Menger determinant, a formula that gives the squared volume of a simplex from its edge lengths. The determinant is positive exactly when the simplex is non-degenerate, meaning it has real volume. For the (4,1) type, the determinant equals (8*alpha - 3) * a^8, so it is positive exactly when alpha > 3/8. For the (3,2) type, it equals (12*alpha - 7) * a^8, positive exactly when alpha > 7/12. Both types are simultaneously non-degenerate exactly when alpha > 7/12, the standard bound in four-dimensional causal dynamical triangulations. On the Lorentzian side, the determinant is strictly negative for all alpha, which under the classical reading means these tuples are never Euclidean-realizable; the Wick rotation is genuinely required to reach a Euclidean geometry. At the physical point alpha = 1, both types reduce to the regular 4-simplex, with determinant 5 * a^8.

What this establishes in plain language is a certified boundary: the framework's library proves exactly where each simplex type becomes geometrically real, and where it does not. The thresholds 3/8 and 7/12 are not fitted numbers but derived consequences of the edge-length assignments. The module does not attempt the next step, the action-level continuation of the full gravitational action, which remains open. But the geometric bridge itself, the map that connects the Lorentzian and Euclidean descriptions of these two building blocks, is now a proved fact in the framework's library.

THEOREM timelike_count_fourOne · spacelike_count_fourOne · timelike_count_threeTwo · spacelike_count_threeTwo · IndisputableMonolith/Gravity/SevenGaps/CausalSimplex4D.lean
timelike_count_fourOne · IndisputableMonolith/Gravity/SevenGaps/CausalSimplex4D.lean:207 
/-- THEOREM (by `decide`): type (4,1) has exactly 4 timelike edges. -/
theorem timelike_count_fourOne :
    (Finset.univ.filter fun e : Fin 10 =>
      isTimelike CausalPentType.fourOne e = true).card = 4 := by
  decide
spacelike_count_fourOne · IndisputableMonolith/Gravity/SevenGaps/CausalSimplex4D.lean:213 
/-- THEOREM (by `decide`): type (4,1) has exactly 6 spacelike edges. -/
theorem spacelike_count_fourOne :
    (Finset.univ.filter fun e : Fin 10 =>
      isTimelike CausalPentType.fourOne e = false).card = 6 := by
  decide
timelike_count_threeTwo · IndisputableMonolith/Gravity/SevenGaps/CausalSimplex4D.lean:219 
/-- THEOREM (by `decide`): type (3,2) has exactly 6 timelike edges. -/
theorem timelike_count_threeTwo :
    (Finset.univ.filter fun e : Fin 10 =>
      isTimelike CausalPentType.threeTwo e = true).card = 6 := by
  decide
spacelike_count_threeTwo · IndisputableMonolith/Gravity/SevenGaps/CausalSimplex4D.lean:225 
/-- THEOREM (by `decide`): type (3,2) has exactly 4 spacelike edges
(3 within the lower slice triangle plus 1 within the upper slice pair). -/
theorem spacelike_count_threeTwo :
    (Finset.univ.filter fun e : Fin 10 =>
      isTimelike CausalPentType.threeTwo e = false).card = 4 := by
  decide
THEOREM wick_involutive · wick_eq_continuation · IndisputableMonolith/Gravity/SevenGaps/CausalSimplex4D.lean
wick_involutive · IndisputableMonolith/Gravity/SevenGaps/CausalSimplex4D.lean:296 
/-- 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
wick_eq_continuation · IndisputableMonolith/Gravity/SevenGaps/CausalSimplex4D.lean:322 
/-- 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
THEOREM cm4_euclidean_fourOne · cm4_euclidean_pos_iff · IndisputableMonolith/Gravity/SevenGaps/CausalSimplex4D.lean
cm4_euclidean_fourOne · IndisputableMonolith/Gravity/SevenGaps/CausalSimplex4D.lean:518 
/-- THEOREM: type (4,1) Euclideanized Cayley-Menger determinant,
`cm4 = (8*alpha - 3) * a^8`.  Cross-check: the AJL volume
`V(4,1) = (a^4/96) * sqrt (8*alpha - 3)` gives
`9216 V^2 = (8*alpha - 3) * a^8`. -/
theorem cm4_euclidean_fourOne (a alpha : ℝ) :
    cm4 (euclideanSqEdges CausalPentType.fourOne a alpha)
      = (8 * alpha - 3) * a ^ 8 := by
  unfold cm4 cmDetN
  rw [cmMatrixN_euclidean_fourOne, det_pentMatrix41]
  ring
cm4_euclidean_pos_iff · IndisputableMonolith/Gravity/SevenGaps/CausalSimplex4D.lean:609 
/-- 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 cm4_euclidean_threeTwo · cm4_euclidean_pos_iff · IndisputableMonolith/Gravity/SevenGaps/CausalSimplex4D.lean
cm4_euclidean_threeTwo · IndisputableMonolith/Gravity/SevenGaps/CausalSimplex4D.lean:529 
/-- THEOREM: type (3,2) Euclideanized Cayley-Menger determinant,
`cm4 = (12*alpha - 7) * a^8`.  Cross-check: the AJL volume
`V(3,2) = (a^4/96) * sqrt (12*alpha - 7)` gives
`9216 V^2 = (12*alpha - 7) * a^8`. -/
theorem cm4_euclidean_threeTwo (a alpha : ℝ) :
    cm4 (euclideanSqEdges CausalPentType.threeTwo a alpha)
      = (12 * alpha - 7) * a ^ 8 := by
  unfold cm4 cmDetN
  rw [cmMatrixN_euclidean_threeTwo, det_pentMatrix32]
  ring
cm4_euclidean_pos_iff · IndisputableMonolith/Gravity/SevenGaps/CausalSimplex4D.lean:609 
/-- 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 cm4_lorentzian_fourOne · cm4_lorentzian_threeTwo · IndisputableMonolith/Gravity/SevenGaps/CausalSimplex4D.lean
cm4_lorentzian_fourOne · IndisputableMonolith/Gravity/SevenGaps/CausalSimplex4D.lean:540 
/-- 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
cm4_lorentzian_threeTwo · IndisputableMonolith/Gravity/SevenGaps/CausalSimplex4D.lean:550 
/-- 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

What this page does not claim

The module does not prove the 4D Cayley-Menger realizability theorem (cm4 > 0 iff embeddable in R^4); that remains open. The module does not formalize the action-level Lorentzian continuation in 4D, including complex dihedral angles and the boost sector. The module does not claim that the Lorentzian tuples are physically realizable; it proves only the sign of the determinant.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND