Gravity Seven Gaps Three Pent Interior Hinge Witness Hinge Link Is Cycle

The minimal interior hinge

In Recognition Science, a framework that derives physical structure from a discrete record of events, the geometry of gravity is built from five-vertex pieces called pents. The declaration hinge_link_is_cycle establishes a precise combinatorial fact about how three such pents can meet. Each pent contains a shared triangle, called the hinge. The theorem proves that the three pents can be arranged so that the edges opposite the hinge, one from each pent, form a closed triangle of their own: vertex 3 connects to 4, 4 to 5, and 5 back to 3. This closed loop is what makes the hinge an interior hinge rather than a boundary feature.

The classical context is Regge calculus, where spacetime is approximated by flat pieces glued together, and curvature is measured by how much the angles around a shared hinge fail to sum to a full turn of 360 degrees. For that deficit to count as genuine interior curvature, the angles must close up in a cycle. The theorem hinge_link_is_cycle proves, by explicit construction, that three pents suffice to create such a cycle. The proof is machine-checked: every incidence fact, such as which tetrahedra the pents share, is verified by computation with no unproved assumptions. A companion result proves that three is the minimum: no complex with fewer than three pents can present the hinge as interior.

What the declaration does not claim is equally important. It is purely combinatorial. It says nothing about whether the edge lengths of these pents can be assigned consistently, nor whether the resulting angle values match those of a causal spacetime. That metric compatibility question remains open and is a separate problem. The theorem licenses calling the angle deficit at this hinge an interior curvature quantity at the incidence level only. It does not by itself establish that the Regge action, the sum of such deficits over all hinges, is physically meaningful for this complex.

The construction is minimal in a strong sense. The three pents are distinct, each shares exactly one tetrahedron with each of the other two, and their triple intersection is exactly the hinge triangle. The link, the structure of edges opposite the hinge, has exactly three vertices and three edges, with every vertex of degree 2. This is the smallest cyclic link possible, and the theorem proves that any complex presenting the hinge as interior must have at least three pents. The three-pent complex therefore attains the lower bound, making it the canonical minimal example for interior hinges in this framework.

/-- THEOREM: the same statement on this module's `linkEdges`, via the
residual identification. -/
theorem hinge_link_is_cycle : IsCycleLink linkEdges := by
  rw [linkEdges_eq_pent_residues]
  exact threePent_hinge_is_interior

/-- **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`): 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 link of the hinge has vertex set
`{3, 4, 5}`. -/
theorem linkVerts_eq : linkVerts = {3, 4, 5} := by decide

What this page does not claim

The theorem does not prove any metric or causal consistency for the three pents. The theorem does not establish that the Regge action is physically meaningful for this complex. The theorem does not claim that the hinge link being a cycle is sufficient for the hinge to be interior in a metric sense.

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: