Gravity Seven Gaps Three Pent Causal Consistency Shared Face Consistency

Shared-face consistency

In geometry, gluing shapes along their boundaries requires care: two triangles glued along an edge must agree on the length of that edge, or the resulting shape is not well-defined. The same concern appears in quantum gravity, where spacetime is built from discrete building blocks called simplices. The declaration shared_face_consistency proves that a particular gluing of three five-vertex simplices, each a four-dimensional analogue of a triangle, is consistent: any edge shared by two of the three pieces is assigned the same squared length by both.

This result is part of a machine-checked library of formal theorems. It states that if two of the three simplices agree on the two vertices of a shared edge, then the squared length they compute for that edge is identical. The proof is structural: all edge lengths come from one global function, causalSqLength, which assigns a value to every pair of vertices based only on whether they lie on the same time slice. Because every simplex pulls its edge lengths back from this single function, any two simplices that share an edge must agree on its length.

The result is not a claim about the physical world. It does not say that this particular gluing is the one realized in nature, nor does it say that the edge-length assignment is unique. The declaration proves a consistency property of a specific, explicit construction: the three simplices, each with three vertices on one time slice and two on the next, are glued around a common hinge edge. The assignment is symmetric, meaning it depends only on whether a pair of vertices lies on the same slice or different slices. Asymmetric assignments, where different simplices might use different rules, are not addressed here.

What the result does establish is that the construction is coherent. It closes a gap in a larger campaign: the existence of an explicit, admissible causal edge-length assignment on this three-simplex complex. The result is one of several that together show each of the three pieces is a standard causal simplex, and that the whole complex is geometrically consistent. It does not, however, address the next step, which is the computation of dihedral angles around the hinge, nor does it touch any claim about the action of the theory.

/-- Shared-face consistency, structurally: whenever two charts send edge
indices to the same global vertex pair (in either order), the induced
squared lengths agree.  This is the "consistent around the cycle"
statement: there is one global length per edge of the complex, full
stop. -/
theorem shared_face_consistency (a alpha : ℝ) (P Q : Fin 5 → Fin 6)
    (e e' : Fin 10)
    (h : (P (pentEdgeVertices e).1 = Q (pentEdgeVertices e').1
          ∧ P (pentEdgeVertices e).2 = Q (pentEdgeVertices e').2)
        ∨ (P (pentEdgeVertices e).1 = Q (pentEdgeVertices e').2
          ∧ P (pentEdgeVertices e).2 = Q (pentEdgeVertices e').1)) :
    inducedSqEdges P a alpha e = inducedSqEdges Q a alpha e' := by
  unfold inducedSqEdges
  rcases h with ⟨h1, h2⟩ | ⟨h1, h2⟩
  · rw [h1, h2]
  · rw [h1, h2, causalSqLength_symm]

/-- THE global causal squared-length assignment on vertex pairs:
same-slice pairs are spacelike (`a^2`), cross-slice pairs timelike
(`-(alpha * a^2)`).  Every pent pulls its edge tuple back from this ONE
function, so shared faces agree by construction. -/
def causalSqLength (a alpha : ℝ) (u v : Fin 6) : ℝ :=
  if slice6 u != slice6 v then -(alpha * a ^ 2) else a ^ 2

What this page does not claim

This gluing is the one realized in physical spacetime. The edge-length assignment around the hinge is unique. The result computes dihedral angles or any action value. The classical equivalence between the Cayley-Menger criterion and embeddability in four dimensions is formalized here.

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: