Encyclopedia Gravity Gravity Seven Gaps Causal Simplex Wick Lorentzian Cm3 Neg Three One

ARTICLE 4 claims 4 theorems

Gravity Seven Gaps Causal Simplex Wick Lorentzian Cm3 Neg Three One

A machine-checked proof shows that the basic building blocks of a causal spacetime cannot exist as ordinary Euclidean shapes, and must be reached by a mathematical rotation.

Verify this page

The Lorentzian tetrahedron

In the approach to quantum gravity called causal dynamical triangulations, spacetime is built from flat tetrahedra glued together between successive slices of space. The theory separates the two kinds of edges a tetrahedron can have: spacelike edges, which lie within a single slice of space, and timelike edges, which connect one slice to the next. The framework's machine-checked library of formal theorems now certifies, for the first time, the Lorentzian side of this construction in three dimensions, the side where timelike edges carry a negative squared length.

The classical fact at the center is that a tetrahedron with a negative squared length on some edges cannot be drawn as an ordinary Euclidean solid. The library proves this exactly: for both allowed tetrahedron types, the Cayley-Menger polynomial, a formula that measures whether six lengths can form a tetrahedron, is strictly negative whenever the timelike parameter alpha is positive. A negative value means the lengths describe no real Euclidean tetrahedron at all. The Lorentzian tetrahedron is therefore a genuinely different object, reached only by a Wick rotation, a formal sign flip on the timelike squared lengths that turns the impossible Lorentzian data into a Euclidean tetrahedron that can be analyzed with ordinary geometry.

The library proves the rotation is coherent. Applying it twice returns the original data, and on the Lorentzian class it acts exactly as the algebraic continuation alpha to -alpha. After rotation, the Euclideanized tetrahedra are non-degenerate, meaning they have nonzero volume, precisely when alpha exceeds a threshold: alpha greater than 1/3 for the type with three vertices on one slice, and alpha greater than 1/2 for the type with two vertices on each slice. Both types are simultaneously valid exactly for alpha greater than 1/2, the standard bound in three-dimensional causal dynamical triangulations. At the physical point alpha = 1, the rotated tetrahedra become regular, and all their dihedral angles are the familiar arccos(1/3), about 70.53 degrees.

In Recognition Science, this result is a step in the Seven-Gaps campaign, a program to certify discrete gravity layer by layer. The declaration establishes the combinatorial classification of the two tetrahedron types, the certified Wick rotation, and the exact non-degeneracy range. It does not attempt the full Lorentzian action, the complex angles and sinh-action sector that would come next, and it does not prove the symbolic reality range of the dihedral angles for all alpha. The library names this honestly: the causal class is defined, the rotation is certified, Euclidean non-degeneracy is proved, and the action-level continuation remains open.

THEOREM cm3_lorentzian_threeOne · cm3_lorentzian_twoTwo · IndisputableMonolith/Gravity/SevenGaps/CausalSimplexWick.lean
cm3_lorentzian_threeOne · IndisputableMonolith/Gravity/SevenGaps/CausalSimplexWick.lean:323 
/-- THEOREM: type (3,1) Lorentzian Cayley-Menger determinant,
`cm3 = -(2 * (3*alpha + 1) * a^6)`: strictly negative for `alpha ≥ 0`,
`a ≠ 0` (see `lorentzian_cm3_neg_threeOne`). -/
theorem cm3_lorentzian_threeOne (a alpha : ℝ) :
    cm3 (lorentzianSqEdges CausalTetType.threeOne a alpha)
      = -(2 * (3 * alpha + 1) * a ^ 6) := by
  have h0 : lorentzianSqEdges CausalTetType.threeOne a alpha 0 = a ^ 2 := rfl
  have h1 : lorentzianSqEdges CausalTetType.threeOne a alpha 1 = a ^ 2 := rfl
  have h2 : lorentzianSqEdges CausalTetType.threeOne a alpha 2
      = -(alpha * a ^ 2) := rfl
  have h3 : lorentzianSqEdges CausalTetType.threeOne a alpha 3 = a ^ 2 := rfl
  have h4 : lorentzianSqEdges CausalTetType.threeOne a alpha 4
      = -(alpha * a ^ 2) := rfl
  have h5 : lorentzianSqEdges CausalTetType.threeOne a alpha 5
      = -(alpha * a ^ 2) := rfl
  unfold cm3
  rw [h0, h1, h2, h3, h4, h5]
  ring
cm3_lorentzian_twoTwo · IndisputableMonolith/Gravity/SevenGaps/CausalSimplexWick.lean:342 
/-- THEOREM: type (2,2) Lorentzian Cayley-Menger determinant,
`cm3 = -(4 * (2*alpha + 1) * a^6)`. -/
theorem cm3_lorentzian_twoTwo (a alpha : ℝ) :
    cm3 (lorentzianSqEdges CausalTetType.twoTwo a alpha)
      = -(4 * (2 * alpha + 1) * a ^ 6) := by
  have h0 : lorentzianSqEdges CausalTetType.twoTwo a alpha 0 = a ^ 2 := rfl
  have h1 : lorentzianSqEdges CausalTetType.twoTwo a alpha 1
      = -(alpha * a ^ 2) := rfl
  have h2 : lorentzianSqEdges CausalTetType.twoTwo a alpha 2
      = -(alpha * a ^ 2) := rfl
  have h3 : lorentzianSqEdges CausalTetType.twoTwo a alpha 3
      = -(alpha * a ^ 2) := rfl
  have h4 : lorentzianSqEdges CausalTetType.twoTwo a alpha 4
      = -(alpha * a ^ 2) := rfl
  have h5 : lorentzianSqEdges CausalTetType.twoTwo a alpha 5 = a ^ 2 := rfl
  unfold cm3
  rw [h0, h1, h2, h3, h4, h5]
  ring
THEOREM wick_involutive · wick_eq_continuation · IndisputableMonolith/Gravity/SevenGaps/CausalSimplexWick.lean
wick_involutive · IndisputableMonolith/Gravity/SevenGaps/CausalSimplexWick.lean:236 
/-- 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
wick_eq_continuation · IndisputableMonolith/Gravity/SevenGaps/CausalSimplexWick.lean:262 
/-- THEOREM: combining the two, the Wick map acts on the causal class as
the continuation `alpha ↦ -alpha`. -/
theorem wick_eq_continuation (ty : CausalTetType) (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 alphaMin_threeOne · alphaMin_twoTwo · cm3_euclidean_pos_iff · IndisputableMonolith/Gravity/SevenGaps/CausalSimplexWick.lean
alphaMin_threeOne · IndisputableMonolith/Gravity/SevenGaps/CausalSimplexWick.lean:391 
theorem alphaMin_threeOne : alphaMin CausalTetType.threeOne = 1 / 3 := rfl
alphaMin_twoTwo · IndisputableMonolith/Gravity/SevenGaps/CausalSimplexWick.lean:393 
theorem alphaMin_twoTwo : alphaMin CausalTetType.twoTwo = 1 / 2 := rfl
cm3_euclidean_pos_iff · IndisputableMonolith/Gravity/SevenGaps/CausalSimplexWick.lean:401 
/-- THEOREM (core, exact range): for `0 < a`, the Euclideanized causal
tetrahedron is non-degenerate (`cm3 > 0`, equivalently positive squared
volume) if and only if `alpha > alphaMin ty`.  The threshold is exact in
both directions. -/
theorem cm3_euclidean_pos_iff (ty : CausalTetType) (a alpha : ℝ)
    (ha : 0 < a) :
    0 < cm3 (euclideanSqEdges ty a alpha) ↔ alphaMin ty < alpha := by
  have h6 : 0 < a ^ 6 := pow_pos ha 6
  cases ty
  · rw [cm3_euclidean_threeOne, alphaMin_threeOne]
    constructor
    · intro h
      by_contra hle
      push_neg at hle
      have hprod : 0 ≤ (1 - 3 * alpha) * a ^ 6 :=
        mul_nonneg (by linarith) h6.le
      linarith
    · intro h
      have hprod : 0 < (3 * alpha - 1) * a ^ 6 :=
        mul_pos (by linarith) h6
      linarith
  · rw [cm3_euclidean_twoTwo, alphaMin_twoTwo]
    constructor
    · intro h
      by_contra hle
      push_neg at hle
      have hprod : 0 ≤ (1 - 2 * alpha) * a ^ 6 :=
        mul_nonneg (by linarith) h6.le
      linarith
    · intro h
      have hprod : 0 < (2 * alpha - 1) * a ^ 6 :=
        mul_pos (by linarith) h6
      linarith
THEOREM euclideanSqEdges_alpha_one · dihedralAngle3_physical · IndisputableMonolith/Gravity/SevenGaps/CausalSimplexWick.lean
euclideanSqEdges_alpha_one · IndisputableMonolith/Gravity/SevenGaps/CausalSimplexWick.lean:528 
/-- THEOREM: at `alpha = 1`, `a = 1`, both causal types Euclideanize to the
regular unit tetrahedron tuple. -/
theorem euclideanSqEdges_alpha_one (ty : CausalTetType) :
    euclideanSqEdges ty 1 1 = regularUnitSqEdges := by
  funext e
  simp only [euclideanSqEdges, regularUnitSqEdges]
  by_cases h : isTimelike ty e = true
  · rw [if_pos h]
    norm_num
  · rw [if_neg h]
    norm_num
dihedralAngle3_physical · IndisputableMonolith/Gravity/SevenGaps/CausalSimplexWick.lean:556 
/-- THEOREM: the Euclidean dihedral angle at every edge of the physical-point
causal tetrahedron is `arccos (1/3)`, hence strictly inside `(0, π)`:
deficit angles at all edges are real and well-defined. -/
theorem dihedralAngle3_physical (ty : CausalTetType) (e : Fin 6) :
    dihedralAngle3 (physicalCausalTet ty) e = Real.arccos (1 / 3) :=
  congrArg Real.arccos (dihedralCos3Sq_alpha_one ty e)

What this page does not claim

The declaration does not prove the action-level Lorentzian continuation, including complex dihedral angles and the sinh-action sector. The declaration does not prove the symbolic reality range of the dihedral angles for all alpha, only at the physical point alpha = 1. The declaration does not connect the Wick rotation to the Recognition Science forcing chain or to the derivation of physical constants.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND