Gravity Seven Gaps Causal Simplex4 D Cm4 Euclidean Degenerate At Min

The degeneracy threshold

The declaration cm4_euclidean_degenerate_at_min is a theorem in the framework's machine-checked library of formal theorems. It concerns a four-dimensional simplex, the simplest geometric shape in four dimensions, which has five vertices and ten edges. In the causal triangulation approach to quantum gravity, spacetime is built from such simplices, and this theorem pins down the precise value of a parameter, called alpha, at which one of these building blocks loses its volume and becomes degenerate, meaning it flattens into a lower-dimensional object.

The classical context comes from the work of Ambjorn, Jurkiewicz, and Loll on causal dynamical triangulations. Their model slices spacetime into layers, and between two layers it fills the gap with two types of four-simplices. The first type, called (4,1), has four vertices on one slice and one on the next. The second, called (3,2), has three on one slice and two on the next. Each edge is classified as spacelike, with squared length a^2, or timelike, with squared length -alpha * a^2 in the Lorentzian regime. The parameter alpha controls the relative size of the timelike edges.

The theorem establishes that for the (4,1) type, the simplex is non-degenerate exactly when alpha is greater than 3/8, and for the (3,2) type, exactly when alpha is greater than 7/12. At these threshold values, the volume squared, computed through the Cayley-Menger determinant, is exactly zero. The proof evaluates this determinant symbolically, giving cm4 = (8*alpha - 3) * a^8 for the (4,1) type and cm4 = (12*alpha - 7) * a^8 for the (3,2) type. This means both types are simultaneously non-degenerate only when alpha exceeds 7/12, which is the standard bound in four-dimensional causal dynamical triangulations.

In Recognition Science, this result is part of a larger campaign to derive physical structure from first principles. The framework's library proves this threshold with no unproved assumptions, and it also proves that the Wick rotation, which flips the sign of timelike squared lengths, is an involution and acts as the algebraic continuation alpha to -alpha. At the physical point alpha = 1, both simplex types reduce to the regular four-simplex, with cm4 = 5 * a^8. The theorem gives an exact, machine-checked boundary for when these spacetime building blocks are geometrically viable.

What this declaration does not claim is equally important. It does not prove that a positive Cayley-Menger determinant means the simplex can be embedded in four-dimensional Euclidean space; that classical equivalence is not formalized in the library for four dimensions. It also does not address the action-level Lorentzian continuation in four dimensions, which involves complex angles and the boost sector of the Regge action. Those remain open targets within the framework, not settled results.

theorem alphaMin_fourOne : alphaMin CausalPentType.fourOne = 3 / 8 := rfl

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

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

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

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

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

/-- 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 (sanity anchor): the regular unit 4-simplex has `cm4 = 5`
(classical: `V = sqrt 5 / 96`, so `9216 V^2 = 5`). -/
theorem cm4_regular_unit : cm4 (fun _ => (1 : ℝ)) = 5 := by
  rw [← euclideanSqEdges_alpha_one CausalPentType.fourOne,
    cm4_euclidean_fourOne]
  norm_num

What this page does not claim

The theorem does not prove that a positive Cayley-Menger determinant implies embeddability in four-dimensional Euclidean space. The theorem does not address the action-level Lorentzian continuation in four dimensions, which remains an open target. The theorem does not claim the physical recognition-to-linking bridge that would connect this geometric result to spatial dimensions.

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: