Gravity Seven Gaps Three Pent Causal Consistency Three Pent Euclidean Admissible

A consistent causal assignment

In the study of discrete spacetime, a common starting point is a simplex: the simplest possible shape in a given number of dimensions, like a triangle in two dimensions or a tetrahedron in three. A causal simplex is one whose edge lengths are assigned so that some pairs of vertices are separated by a timelike interval (a signal could travel between them) and others by a spacelike interval (no signal could). The declaration threePent_euclidean_admissible is a theorem in a machine-checked library of formal theorems. It proves that a specific geometric configuration, made of three such causal simplices glued around a common central triangle, can be given a consistent set of edge lengths.

The configuration in question has six vertices: three forming the central triangle, and three more connected to it. The theorem defines a single global rule for assigning squared lengths to every pair of vertices. Pairs within the same time slice get a positive squared length (spacelike), while pairs in different slices get a negative squared length (timelike), with a parameter alpha controlling the ratio. The central result is that when alpha is greater than 7/12, a specific mathematical condition called the Cayley-Menger determinant, evaluated after a Wick rotation (a standard technique to convert between Lorentzian and Euclidean geometry), is positive for each of the three simplices. This positivity is the criterion for a Euclidean simplex to be nondegenerate, meaning it has real, positive volume and is not flattened.

The theorem's significance is not that it finds a unique or special assignment, but that it shows one exists at all. This closes a specific gap in a broader research program: a prior combinatorial proof had established that this configuration, the minimal one with an interior hinge, could exist, but lacked the explicit length assignment that the current theorem provides. The existence of such an assignment is a necessary precondition for further analysis, such as computing the action or curvature around the hinge. The proof is fully formal, relying only on the standard axioms of the underlying logic, with no unproven assumptions or shortcuts.

What the theorem does not do is also important. It does not claim that this assignment is unique, nor does it classify all possible asymmetric assignments around the hinge. It does not compute the dihedral angles, the angles between the faces of the simplices, which would be needed for a full geometric analysis. It does not address the question of whether the entire configuration can be embedded in a continuous four-dimensional spacetime. Finally, it does not make any statement about the physical action of the configuration; that remains a separate, open problem. The theorem is an existence proof for a specific, symmetric assignment, not a complete physical theory.

/-- THEOREM (per-pent Euclidean admissibility): on the EXACT 4d CDT
range `alpha > 7/12` (with `0 < a`), the Wick image of every pent
satisfies the Cayley-Menger positivity criterion `cm4 > 0` — all three
pents Euclideanize to nondegenerate 4-simplices simultaneously. -/
theorem threePent_euclidean_admissible (a alpha : ℝ) (ha : 0 < a)
    (halpha : 7 / 12 < alpha) :
    0 < cm4 (wick CausalPentType.threeTwo (inducedSqEdges pentAVert a alpha))
      ∧ 0 < cm4 (wick CausalPentType.threeTwo
          (inducedSqEdges pentBVert a alpha))
      ∧ 0 < cm4 (wick CausalPentType.threeTwo
          (inducedSqEdges pentCVert a alpha)) := by
  rw [induced_pentA_eq, induced_pentB_eq, induced_pentC_eq]
  have h := wick_lorentzian_nondegenerate CausalPentType.threeTwo a alpha ha
    (by rw [alphaMin_threeTwo]; exact halpha)
  exact ⟨h, h, h⟩

/-- THEOREM (per-pent Euclidean admissibility): on the EXACT 4d CDT
range `alpha > 7/12` (with `0 < a`), the Wick image of every pent
satisfies the Cayley-Menger positivity criterion `cm4 > 0` — all three
pents Euclideanize to nondegenerate 4-simplices simultaneously. -/
theorem threePent_euclidean_admissible (a alpha : ℝ) (ha : 0 < a)
    (halpha : 7 / 12 < alpha) :
    0 < cm4 (wick CausalPentType.threeTwo (inducedSqEdges pentAVert a alpha))
      ∧ 0 < cm4 (wick CausalPentType.threeTwo
          (inducedSqEdges pentBVert a alpha))
      ∧ 0 < cm4 (wick CausalPentType.threeTwo
          (inducedSqEdges pentCVert a alpha)) := by
  rw [induced_pentA_eq, induced_pentB_eq, induced_pentC_eq]
  have h := wick_lorentzian_nondegenerate CausalPentType.threeTwo a alpha ha
    (by rw [alphaMin_threeTwo]; exact halpha)
  exact ⟨h, h, h⟩

/-- THEOREM (per-pent Euclidean admissibility): on the EXACT 4d CDT
range `alpha > 7/12` (with `0 < a`), the Wick image of every pent
satisfies the Cayley-Menger positivity criterion `cm4 > 0` — all three
pents Euclideanize to nondegenerate 4-simplices simultaneously. -/
theorem threePent_euclidean_admissible (a alpha : ℝ) (ha : 0 < a)
    (halpha : 7 / 12 < alpha) :
    0 < cm4 (wick CausalPentType.threeTwo (inducedSqEdges pentAVert a alpha))
      ∧ 0 < cm4 (wick CausalPentType.threeTwo
          (inducedSqEdges pentBVert a alpha))
      ∧ 0 < cm4 (wick CausalPentType.threeTwo
          (inducedSqEdges pentCVert a alpha)) := by
  rw [induced_pentA_eq, induced_pentB_eq, induced_pentC_eq]
  have h := wick_lorentzian_nondegenerate CausalPentType.threeTwo a alpha ha
    (by rw [alphaMin_threeTwo]; exact halpha)
  exact ⟨h, h, h⟩

What this page does not claim

The theorem does not claim the edge-length assignment is unique. It does not compute the dihedral angles around the hinge. It does not address embedding the whole configuration in continuous 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/ThreePentCausalConsistency.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: