Encyclopedia Gravity Gravity Seven Gaps Glued Pents Hinge Witness Interior Hinge Needs Three Pents

ARTICLE 4 claims 4 theorems

Gravity Seven Gaps Glued Pents Hinge Witness Interior Hinge Needs Three Pents

Two four-dimensional building blocks glued face-to-face cannot create a true interior hinge; the framework proves a third is always required.

Verify this page

The three-pent minimum

In four-dimensional geometry, a hinge is a triangle where several building blocks meet. The Recognition Science framework asks when such a hinge is genuinely interior, meaning the blocks completely surround it in a closed loop, rather than merely touching it from the outside. The machine-checked library of formal theorems proves a precise combinatorial fact: at least three four-dimensional simplices, called pents, must meet around a hinge triangle for it to be interior. This is the declaration interior_hinge_needs_three_pents, a theorem in the framework's library.

The proof works by counting. Around a hinge triangle, each pent contributes exactly one link edge, which is the pair of its vertices not on the triangle. For the hinge to be interior, these link edges must form a cycle, a closed loop. A cycle in a simple graph needs at least three edges, because a single edge cannot close on itself and two edges cannot form a loop on two vertices. Therefore, three pents are the minimum. The theorem is general: it applies to any collection of pents, not just the specific two-pent example the library also analyzes.

The library also examines the concrete case of exactly two pents glued along a shared tetrahedron. In that case, the link edges form a path, not a cycle, so the hinge is a boundary hinge. The dihedral angles at such a hinge sum along an open chain, and any expression shaped like a Regge action is honestly only a hinge angle-sum, not an interior curvature deficit. The two-pent case is impossible for an interior hinge, and the theorem twoPent_hinge_never_interior states this directly.

This result matters because it sets a floor for when a glued-pent expression can be called a Regge action, a discrete model of gravity. The framework does not construct the minimal three-pent complex; that remains a target. The theorem only establishes the counting lower bound. It says nothing about angles, edge lengths, or the physical content of a Regge action, only about the combinatorial incidence structure required for an interior hinge.

THEOREM interior_hinge_needs_three_pents · IndisputableMonolith/Gravity/SevenGaps/GluedPentsHingeWitness.lean
interior_hinge_needs_three_pents · IndisputableMonolith/Gravity/SevenGaps/GluedPentsHingeWitness.lean:308 
/-- **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
THEOREM cycleLink_three_edges · IndisputableMonolith/Gravity/SevenGaps/GluedPentsHingeWitness.lean
cycleLink_three_edges · IndisputableMonolith/Gravity/SevenGaps/GluedPentsHingeWitness.lean:247 
/-- **THEOREM (counting lemma)**: a cyclic link needs at least 3 edges.
Proof: take an edge `e = {a,b}`; degree-2 at `a` gives a second edge
`e' ≠ e` through `a`, degree-2 at `b` gives a second edge `e'' ≠ e`
through `b`; if `e' = e''` then it contains both `a` and `b`, and having
exactly 2 elements it would equal `e` — contradiction.  So `e, e', e''`
are three distinct edges. -/
theorem cycleLink_three_edges {V : Type*} [DecidableEq V]
    (E : Finset (Finset V)) (h : IsCycleLink E) : 3 ≤ E.card := by
  obtain ⟨⟨e, he⟩, hcard, hdeg⟩ := h
  obtain ⟨a, b, hab, heab⟩ := Finset.card_eq_two.mp (hcard e he)
  have ha : a ∈ e := by
    rw [heab]; exact Finset.mem_insert_self a {b}
  have hb : b ∈ e := by
    rw [heab]; exact Finset.mem_insert_of_mem (Finset.mem_singleton_self b)
  -- second edge through a
  have hdega : 1 < (E.filter (fun f => a ∈ f)).card := by
    rw [hdeg a ⟨e, he, ha⟩]; exact one_lt_two
  obtain ⟨e', he'mem, he'ne⟩ := Finset.exists_mem_ne hdega e
  obtain ⟨he'E, hae'⟩ := Finset.mem_filter.mp he'mem
  -- second edge through b
  have hdegb : 1 < (E.filter (fun f => b ∈ f)).card := by
    rw [hdeg b ⟨e, he, hb⟩]; exact one_lt_two
  obtain ⟨e'', he''mem, he''ne⟩ := Finset.exists_mem_ne hdegb e
  obtain ⟨he''E, hbe''⟩ := Finset.mem_filter.mp he''mem
  -- e' and e'' are distinct: otherwise a common edge ⊇ {a,b} of size 2
  -- would equal e
  have hne' : e' ≠ e'' := by
    intro hEq
    have hbe' : b ∈ e' := hEq ▸ hbe''
    have hsub : e ⊆ e' := by
      rw [heab]
      intro x hx
      rcases Finset.mem_insert.mp hx with hxa | hxb
      · exact hxa ▸ hae'
      · exact (Finset.mem_singleton.mp hxb) ▸ hbe'
    have heq : e = e' :=
      Finset.eq_of_subset_of_card_le hsub
        (by rw [hcard e' he'E, hcard e he])
    exact he'ne heq.symm
  -- three distinct edges inside E
  have hnotmem1 : e' ∉ ({e''} : Finset (Finset V)) := by
    intro hmem
    exact hne' (Finset.mem_singleton.mp hmem)
  have hnotmem2 : e ∉ insert e' ({e''} : Finset (Finset V)) := by
    intro hmem
    rcases Finset.mem_insert.mp hmem with hmem' | hmem''
    · exact he'ne hmem'.symm
    · exact he''ne (Finset.mem_singleton.mp hmem'').symm
  have hsub3 : ({e, e', e''} : Finset (Finset V)) ⊆ E := by
    intro f hf
    rcases Finset.mem_insert.mp hf with hf1 | hf'
    · exact hf1 ▸ he
    rcases Finset.mem_insert.mp hf' with hf2 | hf3
    · exact hf2 ▸ he'E
    · exact (Finset.mem_singleton.mp hf3) ▸ he''E
  have hcard3 : ({e, e', e''} : Finset (Finset V)).card = 3 := by
    rw [Finset.card_insert_of_notMem hnotmem2,
      Finset.card_insert_of_notMem hnotmem1, Finset.card_singleton]
  calc 3 = ({e, e', e''} : Finset (Finset V)).card := hcard3.symm
    _ ≤ E.card := Finset.card_le_card hsub3
THEOREM hinge_link_is_path · IndisputableMonolith/Gravity/SevenGaps/GluedPentsHingeWitness.lean
hinge_link_is_path · IndisputableMonolith/Gravity/SevenGaps/GluedPentsHingeWitness.lean:230 
/-- **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 twoPent_hinge_never_interior · IndisputableMonolith/Gravity/SevenGaps/GluedPentsHingeWitness.lean
twoPent_hinge_never_interior · IndisputableMonolith/Gravity/SevenGaps/GluedPentsHingeWitness.lean:318 
/-- **THEOREM (main witness, negative case)**: the two-pent complex can
NEVER present the hinge as an interior hinge: its residual link-edge set
(2 edges) cannot be a cycle. -/
theorem twoPent_hinge_never_interior :
    ¬ IsCycleLink (twoPentComplex.image (fun P => P \ hinge)) := by
  intro h
  have h3 := interior_hinge_needs_three_pents twoPentComplex h
  have h2 : twoPentComplex.card = 2 := by decide
  omega

What this page does not claim

The theorem does not construct the minimal three-pent complex. The theorem says nothing about angles, edge lengths, or the physical content of a Regge action. The theorem does not claim that any three-pent complex automatically yields an interior hinge.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND