Encyclopedia Gravity Gravity Seven Gaps Glued Pents Hinge Witness Hinge Tets Card And Shared

ARTICLE 4 claims 4 theorems

Gravity Seven Gaps Glued Pents Hinge Witness Hinge Tets Card And Shared

A machine-checked proof counts the tetrahedra around a hinge in a two-piece complex, and shows that the hinge is on the boundary, not the interior.

Verify this page

The hinge census

In the geometry of simplicial complexes, a hinge is a shared lower-dimensional face where pieces meet. Consider two four-dimensional simplices, each with five vertices. Glue them along a common tetrahedron, which has four vertices. The hinge in question is a triangle with three vertices, all of which lie inside that shared tetrahedron. The theorem hingeTets_card_and_shared counts the tetrahedra that contain this hinge: there are exactly three, and the shared tetrahedron is one of them.

The three tetrahedra are not symmetric. The shared tetrahedron appears in both pieces. The other two are each exclusive to one piece: one lives only in the first simplex, the other only in the second. This asymmetry is what makes the hinge a boundary feature. Around an interior hinge, the surrounding tetrahedra would form a closed loop. Here they form an open chain, because the two exclusive tetrahedra meet only at the shared one, and that shared tetrahedron is the single connection between them.

The counting lemma behind this is general. A cycle in a simple graph needs at least three edges. Each four-dimensional simplex contributes exactly one edge to the link of the hinge, so a genuine interior hinge requires at least three simplices around the triangle. With only two, a closed loop is impossible. The proof establishes this impossibility directly, and it also shows that the hinge link is a path on three vertices, not a cycle.

In Recognition Science, this result acts as a witness for a larger claim about recognition, the framework's term for a discrete record of events. The framework models gravity as a structure built from such records. The theorem does not construct a full gravity model. It supplies a necessary condition: any expression that looks like a Regge action, a sum over hinge angles, must have a cyclic link at an interior hinge. This two-piece complex fails that test, so its hinge angle-sum is a boundary quantity, not an interior curvature deficit.

The result is a precise negative statement. It does not say that Regge action is wrong, or that the framework has failed. It says that this particular two-piece configuration cannot serve as an interior hinge, and therefore cannot support an interior curvature term. The minimal complex that could do so would need at least three pieces around the hinge. That construction remains open, and this theorem marks the boundary of what the current evidence supports.

THEOREM hingeTets_card_and_shared · IndisputableMonolith/Gravity/SevenGaps/GluedPentsHingeWitness.lean
hingeTets_card_and_shared · IndisputableMonolith/Gravity/SevenGaps/GluedPentsHingeWitness.lean:158 
/-- THEOREM (by `decide`): three tetrahedra contain the hinge, and the
shared tetrahedron is one of them. -/
theorem hingeTets_card_and_shared :
    hingeTets.card = 3 ∧ sharedTet ∈ hingeTets := by decide
THEOREM hingeTets_eq · boundary_tets_belong_to_one_pent · IndisputableMonolith/Gravity/SevenGaps/GluedPentsHingeWitness.lean
hingeTets_eq · IndisputableMonolith/Gravity/SevenGaps/GluedPentsHingeWitness.lean:151 
/-- THEOREM (by `decide`): the tetrahedra of the complex containing the
hinge are exactly `{0,1,2,3}`, `{0,1,2,4}`, `{0,1,2,5}`. -/
theorem hingeTets_eq :
    hingeTets
      = {({0, 1, 2, 3} : Finset (Fin 6)), {0, 1, 2, 4}, {0, 1, 2, 5}} := by
  decide
boundary_tets_belong_to_one_pent · IndisputableMonolith/Gravity/SevenGaps/GluedPentsHingeWitness.lean:175 
/-- 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 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 twoPent_hinge_never_interior · hinge_link_is_path · 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
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⟩

What this page does not claim

The theorem does not construct a three-pent complex with an interior hinge. The theorem does not prove that any Regge action expression is valid or invalid. The theorem does not assign edge lengths, angles, or any metric data to the complex.

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