Gravity Seven Gaps Three Pent Causal Consistency Three Pent Lorentzian Cm4 Neg

The three-pent certificate

In the search for a quantum theory of gravity, one strategy builds spacetime from tiny triangular building blocks, called simplices. A key question is whether these blocks can be glued together consistently. The declaration threePent_lorentzian_cm4_neg is a machine-checked theorem that answers this for a specific configuration of three such blocks, each a 4-simplex with a causal (3,2) signature, sharing a common triangle.

The theorem proves that for any positive scale factor a and any non-negative parameter alpha, the squared length of every edge in these three simplices, as assigned by a single global rule, satisfies a specific inequality. This inequality, expressed through the Cayley-Menger determinant, states that a certain computed value, cm4, is strictly negative for each simplex: cm4 = -((12*alpha + 7) * a^8). This negative value is the Lorentzian condition, meaning the geometry of each block is consistent with the rules of special relativity, with time-like and space-like separations correctly distinguished.

The proof does not stop at the Lorentzian signature. It also shows that after a mathematical operation called a Wick rotation, which converts a Lorentzian geometry into a Euclidean one, the same three simplices become admissible Euclidean 4-simplices. This is true for a specific range of the parameter alpha, namely when alpha is greater than 7/12. In this Euclidean picture, the Cayley-Menger determinant becomes strictly positive, which is the condition for a non-degenerate, genuine 4-simplex. This dual certification, Lorentzian before rotation and Euclidean after, is what makes the assignment physically meaningful.

The significance is that this provides an explicit, consistent causal edge-length assignment for the smallest possible complex with an interior hinge, a point where multiple simplices meet. This closes a specific gap in a larger research program, showing that such a configuration can exist. It does not, however, address what happens with asymmetric assignments or the values of dihedral angles around the hinge, which are needed for the next stage of the theory.

In Recognition Science, this is a theorem, not a model or a hypothesis. It is a proven statement within the framework's machine-checked library, carrying the standard axioms of the ambient type theory. Its role is to provide a concrete, verified object for subsequent work, not to predict a new physical phenomenon.

/-- THEOREM (per-pent Lorentzian Cayley-Menger certificate): every pent
of the complex has `cm4 = -((12*alpha + 7) * a^8) < 0` — the strict CM
negativity of a genuine Lorentzian (3,2) simplex. -/
theorem threePent_lorentzian_cm4_neg (a alpha : ℝ) (ha : 0 < a)
    (halpha : 0 ≤ alpha) :
    cm4 (inducedSqEdges pentAVert a alpha) < 0
      ∧ cm4 (inducedSqEdges pentBVert a alpha) < 0
      ∧ cm4 (inducedSqEdges pentCVert a alpha) < 0 := by
  rw [induced_pentA_eq, induced_pentB_eq, induced_pentC_eq]
  have h := lorentzian_cm4_neg_threeTwo a alpha ha halpha
  exact ⟨h, h, h⟩

/-- THEOREM (per-pent Lorentzian Cayley-Menger certificate): every pent
of the complex has `cm4 = -((12*alpha + 7) * a^8) < 0` — the strict CM
negativity of a genuine Lorentzian (3,2) simplex. -/
theorem threePent_lorentzian_cm4_neg (a alpha : ℝ) (ha : 0 < a)
    (halpha : 0 ≤ alpha) :
    cm4 (inducedSqEdges pentAVert a alpha) < 0
      ∧ cm4 (inducedSqEdges pentBVert a alpha) < 0
      ∧ cm4 (inducedSqEdges pentCVert a alpha) < 0 := by
  rw [induced_pentA_eq, induced_pentB_eq, induced_pentC_eq]
  have h := lorentzian_cm4_neg_threeTwo a alpha ha 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

This theorem does not claim to derive the values of the dihedral angles around the hinge. This theorem does not address the classification of asymmetric causal edge-length assignments. This theorem does not claim that the classical equivalence between a positive Cayley-Menger determinant and embeddability in R^4 is formalized for n=4.

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: