Encyclopedia Gravity Gravity Seven Gaps Three Pent Causal Consistency

ARTICLE 5 claims 5 theorems

Gravity Seven Gaps Three Pent Causal Consistency

A machine-checked proof that three standard causal building blocks can be glued around a shared hinge with consistent edge lengths, a key step in a larger gravity program.

Verify this page

The causal assignment

In the Recognition Science framework's gravity program, spacetime is built from discrete building blocks called pents, which are five-vertex simplices with a causal structure. The framework's machine-checked library of formal theorems has now closed a specific gap in this construction: it proves that three such pents can be arranged around a common interior hinge, a triangle, with a single consistent assignment of edge lengths. The result, named Three-Pent Causal Consistency, is a theorem in the framework's library, meaning it has been verified by a computer against the foundational axioms, with no gaps or unproven assumptions.

The core of the result is a simple, global rule for assigning squared lengths to the six vertices of the complex. Edges lying within the same time slice get a positive squared length, a^2, marking them as spacelike. Edges connecting the hinge triangle on one slice to the three link vertices on the next get a negative squared length, -(alpha * a^2), marking them as timelike. The theorem proves that this single rule, when applied to each of the three pents, makes each one exactly a standard causal (3,2) pent, meaning it has three spacelike edges in one slice and two in the next, with the correct Lorentzian signature. Because all three pents pull their edge data from this one function, they agree on their shared faces by construction, so the whole complex is internally consistent.

The proof goes further than just defining the assignment. It shows each pent is a member of the correct Lorentzian causal class, and that its Cayley-Menger determinant, a quantity that measures whether a simplex is geometrically valid, is negative, as required for a Lorentzian simplex. After a Wick rotation, which is a standard technique to move from Lorentzian to Euclidean signature, the same determinant becomes positive for a specific range of the parameter alpha, namely alpha > 7/12. This confirms the pents are admissible as genuine nondegenerate 4-simplices in the Euclidean regime. A specific non-vacuity check at a = 1 and alpha = 1 shows the construction is not empty: it Wick-rotates to the regular unit 4-simplex.

In Recognition Science, this closes the existential reading of a specific gap, labeled gap6-a, in the campaign to derive gravity from the framework's core principles. The certified non-existence branch of that lane, which would have halted progress, does not fire because an explicit, admissible causal assignment now demonstrably exists. The result does not address the classification of asymmetric assignments, nor does it perform the action-level continuation that would be needed for the next gap, gap6-b. It establishes a concrete, verified object for that next step to attack, but the physical bridge from this combinatorial structure to full gravitational dynamics remains an open target.

THEOREM induced_pentA_eq · induced_pentB_eq · induced_pentC_eq · IndisputableMonolith/Gravity/SevenGaps/ThreePentCausalConsistency.lean
induced_pentA_eq · IndisputableMonolith/Gravity/SevenGaps/ThreePentCausalConsistency.lean:186 
/-- **THEOREM (consistency core, pent A): the induced tuple of pent A is
EXACTLY the standard CDT Lorentzian (3,2) tuple.** -/
theorem induced_pentA_eq (a alpha : ℝ) :
    inducedSqEdges pentAVert a alpha =
      lorentzianSqEdges CausalPentType.threeTwo a alpha := by
  funext e
  fin_cases e <;> rfl
induced_pentB_eq · IndisputableMonolith/Gravity/SevenGaps/ThreePentCausalConsistency.lean:194 
/-- **THEOREM (consistency core, pent B).** -/
theorem induced_pentB_eq (a alpha : ℝ) :
    inducedSqEdges pentBVert a alpha =
      lorentzianSqEdges CausalPentType.threeTwo a alpha := by
  funext e
  fin_cases e <;> rfl
induced_pentC_eq · IndisputableMonolith/Gravity/SevenGaps/ThreePentCausalConsistency.lean:201 
/-- **THEOREM (consistency core, pent C).** -/
theorem induced_pentC_eq (a alpha : ℝ) :
    inducedSqEdges pentCVert a alpha =
      lorentzianSqEdges CausalPentType.threeTwo a alpha := by
  funext e
  fin_cases e <;> rfl
THEOREM threePent_lorentzian_class · threePent_lorentzian_cm4_neg · IndisputableMonolith/Gravity/SevenGaps/ThreePentCausalConsistency.lean
threePent_lorentzian_class · IndisputableMonolith/Gravity/SevenGaps/ThreePentCausalConsistency.lean:210 
/-- THEOREM: each induced tuple is a member of the Lorentzian causal
class of type (3,2). -/
theorem threePent_lorentzian_class (a alpha : ℝ) (ha : 0 < a)
    (halpha : 0 < alpha) :
    inducedSqEdges pentAVert a alpha ∈ LorentzianClass CausalPentType.threeTwo
      ∧ inducedSqEdges pentBVert a alpha
          ∈ LorentzianClass CausalPentType.threeTwo
      ∧ inducedSqEdges pentCVert a alpha
          ∈ LorentzianClass CausalPentType.threeTwo :=
  ⟨⟨a, alpha, ha, halpha, induced_pentA_eq a alpha⟩,
    ⟨a, alpha, ha, halpha, induced_pentB_eq a alpha⟩,
    ⟨a, alpha, ha, halpha, induced_pentC_eq a alpha⟩⟩
threePent_lorentzian_cm4_neg · IndisputableMonolith/Gravity/SevenGaps/ThreePentCausalConsistency.lean:223 
/-- 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 threePent_euclidean_admissible · IndisputableMonolith/Gravity/SevenGaps/ThreePentCausalConsistency.lean
threePent_euclidean_admissible · IndisputableMonolith/Gravity/SevenGaps/ThreePentCausalConsistency.lean:235 
/-- 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 threePent_causal_assignment · IndisputableMonolith/Gravity/SevenGaps/ThreePentCausalConsistency.lean
threePent_causal_assignment · IndisputableMonolith/Gravity/SevenGaps/ThreePentCausalConsistency.lean:310 
/-- **GAP6-A HEADLINE (THEOREM): an explicit admissible causal
edge-length assignment on the minimal three-pent interior-hinge complex
EXISTS.**  On the exact 4d CDT range (`0 < a`, `alpha > 7/12`), the ONE
global assignment `causalSqLength` presents all three pents
simultaneously as standard Lorentzian (3,2) simplices (consistency
core), members of the Lorentzian causal class, with strict Lorentzian
CM negativity and Euclidean CM admissibility after Wick, per pent.
EXISTENCE-ONLY SCOPE: this realizes the symmetric standard CDT slab
assignment; it does not classify asymmetric assignments or hinge-cycle
monodromy.  The certified-non-existence branch of the W3-2 lane does
not fire; gap6-b may proceed against this concrete object. -/
theorem threePent_causal_assignment (a alpha : ℝ) (ha : 0 < a)
    (halpha : 7 / 12 < alpha) :
    (inducedSqEdges pentAVert a alpha
          = lorentzianSqEdges CausalPentType.threeTwo a alpha
        ∧ inducedSqEdges pentBVert a alpha
          = lorentzianSqEdges CausalPentType.threeTwo a alpha
        ∧ inducedSqEdges pentCVert a alpha
          = lorentzianSqEdges CausalPentType.threeTwo a alpha)
      ∧ (inducedSqEdges pentAVert a alpha
            ∈ LorentzianClass CausalPentType.threeTwo
        ∧ inducedSqEdges pentBVert a alpha
            ∈ LorentzianClass CausalPentType.threeTwo
        ∧ inducedSqEdges pentCVert a alpha
            ∈ LorentzianClass CausalPentType.threeTwo)
      ∧ (cm4 (inducedSqEdges pentAVert a alpha) < 0
        ∧ cm4 (inducedSqEdges pentBVert a alpha) < 0
        ∧ cm4 (inducedSqEdges pentCVert a alpha) < 0)
      ∧ (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
  have halpha0 : 0 < alpha := lt_trans (by norm_num) halpha
  exact ⟨⟨induced_pentA_eq a alpha, induced_pentB_eq a alpha,
      induced_pentC_eq a alpha⟩,
    threePent_lorentzian_class a alpha ha halpha0,
    threePent_lorentzian_cm4_neg a alpha ha halpha0.le,
    threePent_euclidean_admissible a alpha ha halpha⟩
THEOREM threePent_causal_assignment · IndisputableMonolith/Gravity/SevenGaps/ThreePentCausalConsistency.lean
threePent_causal_assignment · IndisputableMonolith/Gravity/SevenGaps/ThreePentCausalConsistency.lean:310 
/-- **GAP6-A HEADLINE (THEOREM): an explicit admissible causal
edge-length assignment on the minimal three-pent interior-hinge complex
EXISTS.**  On the exact 4d CDT range (`0 < a`, `alpha > 7/12`), the ONE
global assignment `causalSqLength` presents all three pents
simultaneously as standard Lorentzian (3,2) simplices (consistency
core), members of the Lorentzian causal class, with strict Lorentzian
CM negativity and Euclidean CM admissibility after Wick, per pent.
EXISTENCE-ONLY SCOPE: this realizes the symmetric standard CDT slab
assignment; it does not classify asymmetric assignments or hinge-cycle
monodromy.  The certified-non-existence branch of the W3-2 lane does
not fire; gap6-b may proceed against this concrete object. -/
theorem threePent_causal_assignment (a alpha : ℝ) (ha : 0 < a)
    (halpha : 7 / 12 < alpha) :
    (inducedSqEdges pentAVert a alpha
          = lorentzianSqEdges CausalPentType.threeTwo a alpha
        ∧ inducedSqEdges pentBVert a alpha
          = lorentzianSqEdges CausalPentType.threeTwo a alpha
        ∧ inducedSqEdges pentCVert a alpha
          = lorentzianSqEdges CausalPentType.threeTwo a alpha)
      ∧ (inducedSqEdges pentAVert a alpha
            ∈ LorentzianClass CausalPentType.threeTwo
        ∧ inducedSqEdges pentBVert a alpha
            ∈ LorentzianClass CausalPentType.threeTwo
        ∧ inducedSqEdges pentCVert a alpha
            ∈ LorentzianClass CausalPentType.threeTwo)
      ∧ (cm4 (inducedSqEdges pentAVert a alpha) < 0
        ∧ cm4 (inducedSqEdges pentBVert a alpha) < 0
        ∧ cm4 (inducedSqEdges pentCVert a alpha) < 0)
      ∧ (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
  have halpha0 : 0 < alpha := lt_trans (by norm_num) halpha
  exact ⟨⟨induced_pentA_eq a alpha, induced_pentB_eq a alpha,
      induced_pentC_eq a alpha⟩,
    threePent_lorentzian_class a alpha ha halpha0,
    threePent_lorentzian_cm4_neg a alpha ha halpha0.le,
    threePent_euclidean_admissible a alpha ha halpha⟩

What this page does not claim

This module does not prove the non-existence of asymmetric assignments. This module does not perform the action-level continuation for the complex. This module does not claim that the classical equivalence of the Cayley-Menger determinant with 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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND