Gravity Seven Gaps Three Pent Interior Hinge Witness

The minimal interior hinge

In the piecewise-linear approach to gravity, spacetime is built from flat building blocks glued together. The standard blocks in four dimensions are 4-simplices, the four-dimensional analog of a triangle. In this framework, the framework's library of formal theorems proves a precise combinatorial fact: three such blocks are the minimum needed to make a shared triangle, called a hinge, lie in the interior of the complex rather than on its boundary.

The specific configuration uses three 4-simplices, each containing the same hinge triangle with vertices labeled 0, 1, and 2. The three blocks share this triangle pairwise through tetrahedra, and their triple intersection is exactly the hinge itself. The proof shows that the hinge has a cyclic link: the edges not in the hinge form a triangle 3-4-5-3, and each of those vertices has degree exactly 2. This cycle condition is what makes the hinge interior, because the dihedral angles around it close up in a full turn.

The minimality result is the key theorem. It states that any configuration presenting a hinge as interior must contain at least three 4-simplices, and the constructed complex attains this bound with exactly three. This is a purely combinatorial statement about finite sets, and the library checks every incidence fact by direct computation, with no unproved assumptions.

In Recognition Science, this witness licenses a specific vocabulary. Because the angles around the hinge close in a cycle, one may call the deficit 2π minus the sum of dihedral angles an interior curvature quantity at the incidence level. This is exactly what the Regge action requires combinatorially for an interior hinge. The witness does not, however, provide metric consistency: edge lengths and angle values for three glued causal 4-simplices remain an open question in a separate lane.

The practical consequence is a clean combinatorial foundation. When one asks whether a hinge is truly interior, the answer now has a minimal certificate: three blocks, arranged so their residual edges form a cycle. This gives a concrete starting point for building discrete gravity from the bottom up, with the smallest possible nontrivial interior hinge configuration in hand.

/-- **THEOREM (minimality)**: the three-pent complex attains the proved
lower bound: it has exactly 3 pents, and by the committed counting lemma
(`interior_hinge_needs_three_pents`) ANY family of pents presenting the
hinge as interior has at least 3.  This is THE minimal interior-hinge
configuration. -/
theorem threePent_minimality :
    threePentComplex.card = 3
      ∧ (∀ pents : Finset (Finset (Fin 6)),
          IsCycleLink (pents.image (fun P => P \ hinge)) → 3 ≤ pents.card) :=
  ⟨by decide, fun pents h => interior_hinge_needs_three_pents pents h⟩

/-- THEOREM (by `decide`): the link of the hinge has edge set
`{{3,4}, {4,5}, {3,5}}` — the triangle cycle `3 — 4 — 5 — 3` — with one
edge per pent, three edges in total. -/
theorem linkEdges_eq :
    linkEdges = {({3, 4} : Finset (Fin 6)), {4, 5}, {3, 5}}
      ∧ linkEdges.card = 3 := by decide

/-- THEOREM (by `decide`): every link vertex has degree exactly 2 — the
closed-chain condition a boundary hinge fails (the two-pent path witness
had endpoint degrees 1). -/
theorem linkDegrees :
    linkDegree 3 = 2 ∧ linkDegree 4 = 2 ∧ linkDegree 5 = 2 := by decide

/-- THEOREM (by `decide`): each adjacent pair of pents intersects in a
tetrahedron (4 vertices) containing the hinge — the gluing is
face-to-face around the hinge. -/
theorem pairwise_shared_tets :
    (pentA ∩ pentB = ({0, 1, 2, 4} : Finset (Fin 6))
        ∧ (pentA ∩ pentB).card = 4 ∧ hinge ⊆ pentA ∩ pentB)
      ∧ (pentB ∩ pentC = ({0, 1, 2, 5} : Finset (Fin 6))
        ∧ (pentB ∩ pentC).card = 4 ∧ hinge ⊆ pentB ∩ pentC)
      ∧ (pentA ∩ pentC = ({0, 1, 2, 3} : Finset (Fin 6))
        ∧ (pentA ∩ pentC).card = 4 ∧ hinge ⊆ pentA ∩ pentC) := by decide

/-- THEOREM (by `decide`): the triple intersection of the three pents is
exactly the hinge triangle — the three pents wrap around the hinge and
nothing more. -/
theorem triple_intersection : pentA ∩ pentB ∩ pentC = hinge := by decide

/-- **THEOREM (main witness, cycle case)**: the residual link-edge set of
the three-pent complex satisfies `IsCycleLink` — the hinge `{0,1,2}` is a
GENUINE INTERIOR hinge.  At the incidence level this is exactly what a
Regge deficit `2π − Σθ` at the hinge requires: the dihedral angles close
up in a cycle around the hinge. -/
theorem threePent_hinge_is_interior :
    IsCycleLink (threePentComplex.image (fun P => P \ hinge)) := by
  unfold IsCycleLink
  decide

What this page does not claim

The witness does not prove metric consistency for three glued causal 4-simplices. The witness does not derive the Regge action from first principles. The witness does not address edge-length or causal-structure 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/ThreePentInteriorHingeWitness.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: