Gravity Seven Gaps Causal Simplex4 D Cm Matrix N Euclidean Three Two

The (3,2) simplex matrix

Causal dynamical triangulations (CDT) build spacetime by gluing together simple building blocks called 4-simplices, the four-dimensional analog of triangles. The building blocks come in two types, distinguished by how many of their five vertices lie on successive time slices. The type called (3,2) has three vertices on one slice and two on the next, connected by four spacelike edges (squared length a²) and six timelike edges (squared length -alpha·a² in the Lorentzian regime, with alpha > 0).

The declaration cmMatrixN_euclidean_threeTwo is a theorem stating that the Cayley-Menger matrix for this (3,2) simplex, after a Wick rotation that flips the sign of the timelike squared lengths (alpha ↦ -alpha), equals a specific 6×6 matrix whose entries are built from a² and alpha·a². The Cayley-Menger matrix is a standard tool in geometry: its determinant encodes the squared volume of a simplex. For the (3,2) simplex, the determinant cm4 evaluates exactly to (12·alpha - 7)·a⁸.

This exact expression yields a sharp threshold. The simplex is non-degenerate, meaning its volume is positive, exactly when alpha > 7/12. At alpha = 7/12 the determinant vanishes and the simplex degenerates. For alpha < 7/12 the determinant is negative, which in the classical reading means the tuple of squared edge lengths cannot be realized as a Euclidean 4-simplex. The theorem proves the determinant sign fact; the classical equivalence between a positive determinant and embeddability in R⁴ is not formalized in this repository for dimension four.

In Recognition Science, this result is a certified step in a campaign to bridge the framework's discrete recognition ledger to causal spacetime geometry. The declaration is proved with no gaps in the machine-checked library of formal theorems, with explicit hypotheses such as 0 < a and alphaMin < alpha. The threshold 7/12 is the standard bound in 4D CDT for both simplex types to be simultaneously non-degenerate, matching the known Euclidean-regime condition.

What the declaration does not claim is broader than what it proves. It does not establish that a positive determinant guarantees a geometric realization in four-dimensional Euclidean space; that realizability theorem remains open. It does not attempt the action-level Wick rotation in 4D, which involves complex dihedral angles and the boost sector of the Regge action. And it does not, by itself, derive any physical constant or coupling; it is a geometric fact about a specific building block, not a statement about the universe's content.

/-- THEOREM: the bordered CM matrix of the Euclideanized (4,1) tuple is the
two-parameter matrix at `p = a^2`, `q = alpha * a^2`. -/
theorem cmMatrixN_euclidean_fourOne (a alpha : ℝ) :
    cmMatrixN (pentDistances (euclideanSqEdges CausalPentType.fourOne a alpha))
      = pentMatrix41 (a ^ 2) (alpha * a ^ 2) := by
  ext i j
  fin_cases i <;> fin_cases j <;> rfl

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

What this page does not claim

The declaration does not prove that a positive Cayley-Menger determinant implies a geometric realization in R⁴. The declaration does not attempt the action-level Lorentzian continuation in 4D. The declaration does not derive any physical constant or coupling.

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: