Gravity Seven Gaps Three Pent Interior Hinge Witness Pairwise Shared Tets

The shared tetrahedra

In the geometry of glued simplices, a hinge is a shared face where several pieces meet; here the hinge is a triangle with vertices labeled 0, 1, and 2. The declaration pairwise_shared_tets concerns three five-vertex simplices, called pents, each containing this hinge. It proves that any two of the three pents share exactly one tetrahedron, a four-vertex face, and that this shared tetrahedron always contains the hinge. Concretely, pent A and pent B share the tetrahedron {0,1,2,4}, pent B and pent C share {0,1,2,5}, and pent A and pent C share {0,1,2,3}. Each intersection has exactly four vertices, so the sharing is face-to-face and unique per pair.

This pairwise fact is the load-bearing step in showing that the hinge is a genuine interior hinge, not a boundary one. Around an interior hinge, the neighboring pieces close up in a cycle; here the three shared tetrahedra leave three residual edges, {3,4}, {4,5}, and {3,5}, which form the triangle cycle 3-4-5-3. The theorems linkEdges_eq and linkDegrees confirm that this cycle has exactly three edges and that every vertex in it has degree 2, the signature of a closed loop. The minimality theorem threePent_minimality then states that three pents are both necessary and sufficient for such an interior hinge, relying on a separate counting lemma that any complex presenting the hinge as interior needs at least three pents.

In Recognition Science, this combinatorial result licenses a specific vocabulary: the deficit 2π minus the sum of dihedral angles at this hinge may be called an interior curvature quantity at the incidence level. Because the angles close up in a cycle, comparing their sum against a full turn is what Regge action at an interior hinge requires combinatorially. The declaration does not, however, provide the metric side: it says nothing about edge lengths or causal structure for three glued causal pents. Whether consistent (4,1)/(3,2) edge-length assignments exist around the cycle, and what the resulting angle values are, remains an open question in a separate lane.

The proof is a finite incidence fact, checked by the kernel's decide tactic with no new axioms. The pents themselves are definitional choices, models of simplices as finite sets of six vertices. What is proved is the incidence structure: the sharing pattern, the cycle, and the minimality. What is not proved is any metric or causal consistency for those pents, which the framework explicitly leaves open.

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

No metric or causal-structure consistency for three glued causal pents is established. No claim about edge lengths or angle values is made. The declaration does not by itself prove that the hinge is physical; it proves only the incidence-level cycle.

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: