Gravity Seven Gaps Glued Pents Hinge Witness Boundary Tets Belong To One Pent

The boundary tetrahedra

In four-dimensional geometry, a 4-simplex (the analogue of a tetrahedron in one higher dimension) is bounded by five tetrahedral faces. When two such 4-simplices, or "pents," are glued along one shared tetrahedron, the resulting complex has a natural hinge: the triangular face common to both pieces. The declaration boundary_tets_belong_to_one_pent establishes, with a kernel-checked proof, exactly which tetrahedra of the complex contain this hinge and whether each belongs to one or both of the original pents.

The concrete complex studied here uses two pents on a six-vertex set: pentA = {0,1,2,3,4} and pentB = {0,1,2,3,5}, sharing exactly the tetrahedron {0,1,2,3}. The hinge is the triangle {0,1,2}. The theorem proves three facts. First, the tetrahedron {0,1,2,4} lies inside pentA but not pentB. Second, the tetrahedron {0,1,2,5} lies inside pentB but not pentA. Third, the shared tetrahedron {0,1,2,3} lies inside both. In plain terms: around the hinge, two of the three tetrahedra are each owned by a single pent, while the third is common to both.

This combinatorial fact matters because it determines the geometry of the hinge's link, the set of edges that connect the hinge to the rest of the complex. The link here is the path 4-3-5, not a cycle. A cycle would require at least three edges and hence at least three pents around the hinge; with only two pents, the hinge is a boundary hinge, not an interior one. The theorem interior_hinge_needs_three_pents proves this general counting bound: a genuine interior hinge in a simplicial complex needs at least three 4-simplices around the triangle.

What the declaration does not claim is equally precise. It does not assert that any physical curvature or angle sum exists at the hinge; the module is purely combinatorial, with no edge lengths or angles. It does not license calling any two-pent expression a "Regge action." The honest characterization is that the hinge angle-sum at this boundary is an exterior-angle quantity, not an interior deficit. The minimal interior-hinge complex, a cyclic gluing of three or more pents, remains a target for future construction.

/-- THEOREM (by `decide`): the two non-shared hinge tetrahedra each belong
to exactly one pent (they are BOUNDARY tetrahedra of the complex), while
the shared tetrahedron belongs to both. -/
theorem boundary_tets_belong_to_one_pent :
    (({0, 1, 2, 4} : Finset (Fin 6)) ⊆ pentA
        ∧ ¬ ({0, 1, 2, 4} : Finset (Fin 6)) ⊆ pentB)
      ∧ (({0, 1, 2, 5} : Finset (Fin 6)) ⊆ pentB
        ∧ ¬ ({0, 1, 2, 5} : Finset (Fin 6)) ⊆ pentA)
      ∧ (sharedTet ⊆ pentA ∧ sharedTet ⊆ pentB) := 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

/-- THEOREM (by `decide`): the link of the hinge has edge set
`{{3,4}, {3,5}}`: one edge per pent (edge `{3,4}` from `pentA`, edge
`{3,5}` from `pentB`), two edges in total. -/
theorem linkEdges_eq :
    linkEdges = {({3, 4} : Finset (Fin 6)), {3, 5}}
      ∧ linkEdges.card = 2 := by decide

/-- **THEOREM (main witness, path case)**: the link of the hinge triangle
`{0,1,2}` in the two-pent complex is a PATH: `4 — 3 — 5`, with the
midpoint `3` contributed by the shared tetrahedron.  The hinge is a
BOUNDARY hinge: dihedral angles at it form an open angle-sum, not an
interior deficit. -/
theorem hinge_link_is_path : ∃ a b c : Fin 6, IsPathLinkOn a b c :=
  ⟨4, 3, 5, by unfold IsPathLinkOn; decide⟩

/-- **THEOREM (minimal interior-hinge requirement)**: since each pent
containing the hinge contributes exactly one link edge (its residual pair
`P \ hinge`), a genuine interior hinge — a cyclic link — requires at least
THREE 4-simplices around the hinge triangle. -/
theorem interior_hinge_needs_three_pents
    (pents : Finset (Finset (Fin 6)))
    (hcycle : IsCycleLink (pents.image (fun P => P \ hinge))) :
    3 ≤ pents.card :=
  le_trans (cycleLink_three_edges _ hcycle) Finset.card_image_le

What this page does not claim

No edge lengths, angles, or metric data are involved in this theorem. The phrase "Regge action" is not licensed for any two-pent expression by this result. The theorem does not construct an interior hinge; it only proves the impossibility with two pents.

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/GluedPentsHingeWitness.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: