Gravity Seven Gaps Three Pent Interior Hinge Witness Pairwise Shared Tets Unique

The three-pent witness

In discrete geometry, a simplex is the simplest shape in a given number of dimensions: a point, a line segment, a triangle, a tetrahedron, and so on. A four-dimensional simplex, called a pent, has five vertices. The declaration pairwise_shared_tets_unique concerns three such pents, each built on the six labels 0 through 5, and each containing the same hinge triangle with vertices 0, 1, and 2.

The theorem states that any two of the three pents share exactly one tetrahedron, and that this shared tetrahedron is unique. Pent A and pent B share only the tetrahedron {0,1,2,4}; pent B and pent C share only {0,1,2,5}; pent A and pent C share only {0,1,2,3}. No other four-vertex overlap exists between any pair. The three pents together intersect in exactly the hinge triangle itself, nothing more.

This uniqueness is what makes the configuration a clean witness. Around the hinge, the three pents leave three leftover edges: {3,4}, {4,5}, and {3,5}. Those three edges form a triangle cycle, which means the hinge is a genuine interior hinge, not a boundary hinge. The machine-checked library of formal theorems proves this cycle property, along with the fact that each vertex in the cycle has degree exactly two. The minimality theorem goes further: any collection of pents presenting the hinge as interior must contain at least three pents, so this three-pent complex is the smallest possible example.

In Recognition Science, this combinatorial fact licenses a specific move. The framework models the deficit angle at an interior hinge as a full turn minus the sum of dihedral angles around it. The cycle property is exactly what that comparison requires at the incidence level. The witness does not, however, provide metric consistency: it says nothing about whether edge lengths or causal structure can be assigned coherently around the cycle. That question remains open, a separate lane from the purely combinatorial result proved here.

/-- THEOREM (by `decide`): each pair of pents shares EXACTLY ONE
tetrahedral face (the intersection of their 4-element subset families is
a singleton). -/
theorem pairwise_shared_tets_unique :
    Finset.powersetCard 4 pentA ∩ Finset.powersetCard 4 pentB
        = {({0, 1, 2, 4} : Finset (Fin 6))}
      ∧ Finset.powersetCard 4 pentB ∩ Finset.powersetCard 4 pentC
        = {({0, 1, 2, 5} : Finset (Fin 6))}
      ∧ Finset.powersetCard 4 pentA ∩ Finset.powersetCard 4 pentC
        = {({0, 1, 2, 3} : Finset (Fin 6))} := 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: 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⟩

What this page does not claim

The witness does not prove any metric or causal-structure consistency for the three glued pents. The declaration does not establish that the hinge is interior in any continuous geometric sense. The minimality theorem does not apply to complexes where pents are not glued face-to-face.

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: