Encyclopedia Gravity Gravity Seven Gaps Three Pent Causal Consistency Hinge Edges Spacelike

ARTICLE 3 claims 3 theorems

Gravity Seven Gaps Three Pent Causal Consistency Hinge Edges Spacelike

In a discrete model of spacetime, a small triangle of edges is shown to be spacelike, meaning its squared length is positive, a fact that lets three standard causal building blocks fit together consistently.

Verify this page

The spacelike hinge

In the framework's discrete model of spacetime, a recognition ledger records events and the connections between them as a finite graph. The declaration hinge_edges_spacelike is a theorem about one small piece of that graph: a triangle of three vertices, called the hinge, and the three edges that connect them. The theorem states that the squared length of each of these three edges is a², a positive number. In the model's causal language, a positive squared length marks an edge as spacelike, meaning the two events it connects are separated in space, not in time.

The theorem is part of a larger construction called the three-pent complex. The complex glues three five-vertex building blocks, each a standard causal (3,2) simplex, around the hinge triangle. The declaration hinge_edges_spacelike is one of three causal-type certificates: it confirms the hinge is spacelike, a second theorem confirms the outer link cycle is spacelike, and a third confirms the nine edges running from the hinge to the links are timelike, with squared length −(α·a²). Together these certificates establish that the three pents fit together with a consistent causal structure, not just as a combinatorial shape but as a geometric one with well-defined edge lengths.

The hinge theorem alone does not prove the whole construction works. It is a single ingredient in a larger package. The package's headline theorem, threePent_causal_assignment, combines the hinge certificate with the others to show that, for any positive scale a and any α greater than 7/12, all three pents are simultaneously admissible causal simplices. The hinge theorem is the piece that guarantees the central triangle, the place where the three pents meet, has the right causal character. Without it, the gluing would be geometrically inconsistent at the very core.

The theorem does not claim that this is the only way to assign causal edge lengths around the hinge. The construction realizes one specific, symmetric assignment where lengths depend only on whether an edge lies within a slice or crosses between slices. Other, asymmetric assignments are not addressed. The theorem also does not compute the dihedral angles around the hinge, which would be needed to measure curvature, and it does not claim that the Euclideanized pents are embeddable in ordinary four-dimensional space; that classical equivalence is not formalized in the framework's library. The hinge theorem is a certificate of causal type, nothing more and nothing less.

THEOREM hinge_edges_spacelike · IndisputableMonolith/Gravity/SevenGaps/ThreePentCausalConsistency.lean
hinge_edges_spacelike · IndisputableMonolith/Gravity/SevenGaps/ThreePentCausalConsistency.lean:253 
/-- THEOREM: the three hinge edges `{0,1}, {0,2}, {1,2}` are spacelike
(squared length `a^2`). -/
theorem hinge_edges_spacelike (a alpha : ℝ) :
    causalSqLength a alpha 0 1 = a ^ 2
      ∧ causalSqLength a alpha 0 2 = a ^ 2
      ∧ causalSqLength a alpha 1 2 = a ^ 2 :=
  ⟨rfl, rfl, rfl⟩
THEOREM hinge_edges_spacelike · link_edges_spacelike · cross_edges_timelike · IndisputableMonolith/Gravity/SevenGaps/ThreePentCausalConsistency.lean
hinge_edges_spacelike · IndisputableMonolith/Gravity/SevenGaps/ThreePentCausalConsistency.lean:253 
/-- THEOREM: the three hinge edges `{0,1}, {0,2}, {1,2}` are spacelike
(squared length `a^2`). -/
theorem hinge_edges_spacelike (a alpha : ℝ) :
    causalSqLength a alpha 0 1 = a ^ 2
      ∧ causalSqLength a alpha 0 2 = a ^ 2
      ∧ causalSqLength a alpha 1 2 = a ^ 2 :=
  ⟨rfl, rfl, rfl⟩
link_edges_spacelike · IndisputableMonolith/Gravity/SevenGaps/ThreePentCausalConsistency.lean:261 
/-- THEOREM: the three link-cycle edges `{3,4}, {4,5}, {3,5}` (one per
pent: the residual pair) are spacelike (squared length `a^2`) — the
hinge link `3-4-5-3` is a spacelike cycle on slice `t+1`. -/
theorem link_edges_spacelike (a alpha : ℝ) :
    causalSqLength a alpha 3 4 = a ^ 2
      ∧ causalSqLength a alpha 4 5 = a ^ 2
      ∧ causalSqLength a alpha 3 5 = a ^ 2 :=
  ⟨rfl, rfl, rfl⟩
cross_edges_timelike · IndisputableMonolith/Gravity/SevenGaps/ThreePentCausalConsistency.lean:270 
/-- THEOREM: all nine hinge-to-link edges are timelike (squared length
`-(alpha * a^2)`). -/
theorem cross_edges_timelike (a alpha : ℝ) :
    ∀ u v : Fin 6, u ∈ GluedPentsHingeWitness.hinge →
      v ∈ ThreePentInteriorHingeWitness.linkVerts →
      causalSqLength a alpha u v = -(alpha * a ^ 2) := by
  intro u v hu hv
  fin_cases u <;> fin_cases v <;>
    first
      | rfl
      | exact absurd hu (by decide)
      | exact absurd hv (by decide)
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

The theorem does not claim that the Euclideanized pents are embeddable in R^4. The theorem does not compute the dihedral angles around the hinge. The theorem does not address asymmetric causal edge-length assignments.

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