Gravity Seven Gaps Three Pent Interior Hinge Witness Triple Intersection

The triple intersection

A pent (a five-vertex simplex, the four-dimensional analogue of a triangle) can be glued to another pent along a shared tetrahedron. The declaration triple_intersection concerns a specific arrangement of three such pents, each containing the same triangle {0,1,2}. The theorem states that the common intersection of all three pents is exactly that triangle: pentA ∩ pentB ∩ pentC = {0,1,2}. This is a combinatorial fact about finite sets, checked by the machine.

Why does this matter? The three pents are glued face-to-face: each pair shares exactly one tetrahedron (a four-vertex set) that contains the hinge triangle. The triple intersection being exactly the hinge means the three tetrahedra meet only along that triangle, with no additional overlap. This is what makes the hinge a genuine interior hinge of the complex, a point where the surrounding structure closes up in a cycle. The framework's library proves the hinge link (the edges left after removing the hinge vertices) forms a triangle cycle, and that three pents are the minimum needed to achieve this.

In Recognition Science, this witness licenses calling a deficit 2π − Σθ at this hinge an interior curvature quantity at the incidence level. The dihedral angles around the hinge close up in a cycle, so their sum is compared against a full turn, which is what Regge action at an interior hinge requires combinatorially. This is a MODEL of the combinatorial data, with THEOREM-level incidence facts about it.

The declaration does not claim anything about metric geometry. It does not provide edge-length or causal-structure consistency for three glued causal pents, nor does it give the resulting angle values. That metric compatibility question remains OPEN and is a separate lane. The theorem is purely combinatorial: it establishes the incidence structure, not the physics that might live on it.

/-- 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 (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 (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

/-- **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⟩

What this page does not claim

The declaration does not establish metric compatibility or edge-length consistency for the three pents. It does not provide the actual dihedral angle values around the hinge. It does not claim the hinge is interior in a metric or causal sense, only combinatorially.

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: