IndisputableMonolith.Gravity.SevenGaps.GluedPentsHingeWitness

   1import Mathlib
   2
   3/-!
   4# Glued-Pents Hinge Witness: two 4-simplices sharing a tetrahedron give a PATH link, not a cycle
   5
   6Panel P1-remainder live bet C12; witness gates whether glued-pent expressions
   7may be called Regge action.
   8
   9## What this module witnesses
  10
  11The concrete two-pent complex: two 4-simplices ("pents")
  12
  13* `pentA = {0,1,2,3,4}` and `pentB = {0,1,2,3,5}` on the vertex set `Fin 6`,
  14
  15sharing EXACTLY ONE tetrahedral face `sharedTet = {0,1,2,3}` (proved:
  16`shared_tets_unique`).  At the chosen hinge triangle `hinge = {0,1,2}` the
  17incidence data is computed and kernel-checked by `decide`:
  18
  19* the tetrahedra of the complex containing the hinge are exactly
  20  `{0,1,2,3}` (in BOTH pents), `{0,1,2,4}` (only in `pentA`), and
  21  `{0,1,2,5}` (only in `pentB`) — `hingeTets_eq`, `pentA_hinge_tets`,
  22  `pentB_hinge_tets`, `boundary_tets_belong_to_one_pent`;
  23* the link of the hinge has vertex set `{3,4,5}` (`linkVerts_eq`) and edge
  24  set `{{3,4},{3,5}}` (`linkEdges_eq`): each pent containing the hinge
  25  contributes exactly one link edge, namely its residual vertex pair
  26  `P \ hinge` (`linkEdges_eq_pent_residues`);
  27* the two link edges chain through the single shared-tetrahedron vertex 3
  28  (`link_edges_chain_through_shared`): the link is the PATH `4 — 3 — 5`.
  29
  30## The honest characterization (do-not-overclaim clause)
  31
  32**`hinge_link_is_path`**: the hinge link is a path on three vertices with
  33two edges (endpoint degrees 1, midpoint degree 2:
  34`linkDegree_four`, `linkDegree_five`, `linkDegree_three`).  It is NOT a
  35cycle (`hinge_link_not_cycle`).  Therefore the hinge `{0,1,2}` of the
  36two-pent complex is a BOUNDARY hinge: the dihedral angles at it sum along
  37an open chain, and any "Regge action"-shaped expression evaluated on this
  38complex at this hinge is honestly only a *hinge angle-sum*.  A curvature
  39deficit `2π − Σθ` at this hinge is a boundary (exterior-angle) quantity,
  40not an interior deficit.
  41
  42**Why two pents can never do better** (the counting lemma): a cyclic link
  43in a simple graph needs at least 3 edges (`cycleLink_three_edges`: every
  44vertex of a cycle has degree 2, and two distinct 2-element edges cannot
  45close up on two vertices).  Each 4-simplex containing the hinge triangle
  46contributes exactly one link edge (its residual pair), so a genuine
  47interior hinge needs at least THREE 4-simplices around the triangle
  48(`interior_hinge_needs_three_pents`); with two pents it is impossible
  49(`twoPent_hinge_never_interior`).  The minimal interior-hinge complex is
  50therefore a cyclic gluing of ≥ 3 pents around the triangle, which this
  51module does NOT construct; that remains the gate for calling any
  52glued-pent expression a Regge action.
  53
  54## Honesty tiers
  55
  56* THEOREM: every declared theorem below is proved with zero sorry, zero
  57  admit, zero new axioms; the finite incidence facts are kernel-checked by
  58  `decide` (no `native_decide`), and `cycleLink_three_edges` /
  59  `interior_hinge_needs_three_pents` are general structural proofs.
  60* MODEL: `pentA`, `pentB`, `sharedTet`, `hinge`, `twoPentComplex`, `tets`,
  61  `hingeTets`, `linkVerts`, `linkEdges`, `linkDegree`, `IsPathLinkOn`,
  62  `IsCycleLink` are definitional encodings (vertex-set combinatorics of
  63  the glued complex; simplices as `Finset (Fin 6)`).  This is a purely
  64  combinatorial layer: no edge lengths, no angles, no analysis.  The
  65  causal 4-simplex classes of `CausalSimplex4D` carry edge-length data on
  66  a SINGLE pent; the present module supplies the missing complex-level
  67  incidence layer and is import-independent of it.
  68
  69## Relation to the mission wording
  70
  71Two pents glued along one shared tetrahedron canNOT produce a genuine
  72interior hinge: the link of the shared triangle is a path (open chain),
  73not a cycle.  This module states and proves exactly that
  74(`hinge_link_is_path`, `hinge_link_not_cycle`) and proves the minimal
  75requirement for an interior hinge (`interior_hinge_needs_three_pents`).
  76No overclaim: no statement here licenses the phrase "Regge action" for
  77any two-pent expression.
  78-/
  79
  80namespace IndisputableMonolith
  81namespace Gravity
  82namespace SevenGaps
  83namespace GluedPentsHingeWitness
  84
  85open Finset
  86
  87/-! ## §1. The two-pent complex (MODEL: concrete combinatorial data) -/
  88
  89/-- First 4-simplex (pent): vertices `{0,1,2,3,4}`. -/
  90def pentA : Finset (Fin 6) := {0, 1, 2, 3, 4}
  91
  92/-- Second 4-simplex (pent): vertices `{0,1,2,3,5}`. -/
  93def pentB : Finset (Fin 6) := {0, 1, 2, 3, 5}
  94
  95/-- The shared tetrahedral face `{0,1,2,3}`. -/
  96def sharedTet : Finset (Fin 6) := {0, 1, 2, 3}
  97
  98/-- The hinge triangle `{0,1,2}`, a 2-face of the shared tetrahedron. -/
  99def hinge : Finset (Fin 6) := {0, 1, 2}
 100
 101/-- The two-pent complex, presented by its maximal simplices. -/
 102def twoPentComplex : Finset (Finset (Fin 6)) := {pentA, pentB}
 103
 104/-- All tetrahedra (3-faces) of the complex: the 4-element subsets of the
 105pents. -/
 106def tets : Finset (Finset (Fin 6)) :=
 107  twoPentComplex.biUnion (Finset.powersetCard 4)
 108
 109/-- The tetrahedra of the complex containing the hinge triangle. -/
 110def hingeTets : Finset (Finset (Fin 6)) :=
 111  tets.filter (fun t => hinge ⊆ t)
 112
 113/-- Link vertices of the hinge: vertices `v ∉ hinge` with
 114`hinge ∪ {v}` a tetrahedron of the complex. -/
 115def linkVerts : Finset (Fin 6) :=
 116  Finset.univ.filter (fun v => v ∉ hinge ∧ insert v hinge ∈ tets)
 117
 118/-- Link edges of the hinge: vertex pairs `E` disjoint from the hinge with
 119`hinge ∪ E` a pent of the complex. -/
 120def linkEdges : Finset (Finset (Fin 6)) :=
 121  (Finset.univ.powersetCard 2).filter
 122    (fun E => E ∩ hinge = ∅ ∧ hinge ∪ E ∈ twoPentComplex)
 123
 124/-- Degree of a vertex in the link graph of the hinge. -/
 125def linkDegree (v : Fin 6) : ℕ :=
 126  (linkEdges.filter (fun e => v ∈ e)).card
 127
 128/-! ## §2. Basic incidence facts (THEOREM, kernel `decide`) -/
 129
 130/-- THEOREM (by `decide`): both pents are genuine 4-simplices (5 distinct
 131vertices) and they are distinct. -/
 132theorem pents_are_distinct_foursimplices :
 133    pentA.card = 5 ∧ pentB.card = 5 ∧ pentA ≠ pentB := by decide
 134
 135/-- THEOREM (by `decide`): the pents intersect exactly in the shared
 136tetrahedron, which has 4 vertices and contains the hinge triangle
 137(3 vertices). -/
 138theorem shared_face_data :
 139    pentA ∩ pentB = sharedTet ∧ sharedTet.card = 4
 140      ∧ hinge.card = 3 ∧ hinge ⊆ sharedTet := by decide
 141
 142/-- THEOREM (by `decide`): the pents share EXACTLY ONE tetrahedral face,
 143namely `sharedTet` (the intersection of their 4-element subset families is
 144the singleton `{sharedTet}`). -/
 145theorem shared_tets_unique :
 146    Finset.powersetCard 4 pentA ∩ Finset.powersetCard 4 pentB
 147      = {sharedTet} := by decide
 148
 149/-! ## §3. The hinge incidence data (THEOREM, kernel `decide`) -/
 150
 151/-- THEOREM (by `decide`): the tetrahedra of the complex containing the
 152hinge are exactly `{0,1,2,3}`, `{0,1,2,4}`, `{0,1,2,5}`. -/
 153theorem hingeTets_eq :
 154    hingeTets
 155      = {({0, 1, 2, 3} : Finset (Fin 6)), {0, 1, 2, 4}, {0, 1, 2, 5}} := by
 156  decide
 157
 158/-- THEOREM (by `decide`): three tetrahedra contain the hinge, and the
 159shared tetrahedron is one of them. -/
 160theorem hingeTets_card_and_shared :
 161    hingeTets.card = 3 ∧ sharedTet ∈ hingeTets := by decide
 162
 163/-- THEOREM (by `decide`): within `pentA`, the tetrahedra containing the
 164hinge are `{0,1,2,3}` (shared) and `{0,1,2,4}` (private to `pentA`). -/
 165theorem pentA_hinge_tets :
 166    (Finset.powersetCard 4 pentA).filter (fun t => hinge ⊆ t)
 167      = {({0, 1, 2, 3} : Finset (Fin 6)), {0, 1, 2, 4}} := by decide
 168
 169/-- THEOREM (by `decide`): within `pentB`, the tetrahedra containing the
 170hinge are `{0,1,2,3}` (shared) and `{0,1,2,5}` (private to `pentB`). -/
 171theorem pentB_hinge_tets :
 172    (Finset.powersetCard 4 pentB).filter (fun t => hinge ⊆ t)
 173      = {({0, 1, 2, 3} : Finset (Fin 6)), {0, 1, 2, 5}} := by decide
 174
 175/-- THEOREM (by `decide`): the two non-shared hinge tetrahedra each belong
 176to exactly one pent (they are BOUNDARY tetrahedra of the complex), while
 177the shared tetrahedron belongs to both. -/
 178theorem boundary_tets_belong_to_one_pent :
 179    (({0, 1, 2, 4} : Finset (Fin 6)) ⊆ pentA
 180        ∧ ¬ ({0, 1, 2, 4} : Finset (Fin 6)) ⊆ pentB)
 181      ∧ (({0, 1, 2, 5} : Finset (Fin 6)) ⊆ pentB
 182        ∧ ¬ ({0, 1, 2, 5} : Finset (Fin 6)) ⊆ pentA)
 183      ∧ (sharedTet ⊆ pentA ∧ sharedTet ⊆ pentB) := by decide
 184
 185/-! ## §4. The hinge link: vertex set, edge set, degrees
 186(THEOREM, kernel `decide`) -/
 187
 188/-- THEOREM (by `decide`): the link of the hinge has vertex set
 189`{3, 4, 5}`. -/
 190theorem linkVerts_eq : linkVerts = {3, 4, 5} := by decide
 191
 192/-- THEOREM (by `decide`): the link of the hinge has edge set
 193`{{3,4}, {3,5}}`: one edge per pent (edge `{3,4}` from `pentA`, edge
 194`{3,5}` from `pentB`), two edges in total. -/
 195theorem linkEdges_eq :
 196    linkEdges = {({3, 4} : Finset (Fin 6)), {3, 5}}
 197      ∧ linkEdges.card = 2 := by decide
 198
 199/-- THEOREM (by `decide`): the link edges are exactly the residual pairs
 200`P \ hinge` of the pents — each 4-simplex containing the hinge contributes
 201exactly one link edge. -/
 202theorem linkEdges_eq_pent_residues :
 203    linkEdges = twoPentComplex.image (fun P => P \ hinge)
 204      ∧ pentA \ hinge = ({3, 4} : Finset (Fin 6))
 205      ∧ pentB \ hinge = ({3, 5} : Finset (Fin 6)) := by decide
 206
 207/-- THEOREM (by `decide`): the two link edges chain through the single
 208residual vertex `3` of the shared tetrahedron: the link is the open chain
 209`4 — 3 — 5`, hinged at the shared-tet vertex. -/
 210theorem link_edges_chain_through_shared :
 211    (({3, 4} : Finset (Fin 6)) ∩ ({3, 5} : Finset (Fin 6)))
 212        = ({3} : Finset (Fin 6))
 213      ∧ sharedTet \ hinge = ({3} : Finset (Fin 6)) := by decide
 214
 215/-- THEOREM (by `decide`): link-graph degrees — midpoint `3` has degree 2,
 216endpoints `4` and `5` have degree 1.  Degree-1 vertices are exactly what a
 217cyclic link forbids. -/
 218theorem linkDegrees :
 219    linkDegree 3 = 2 ∧ linkDegree 4 = 1 ∧ linkDegree 5 = 1 := by decide
 220
 221/-! ## §5. The honest characterization: PATH, not cycle -/
 222
 223/-- The hinge link is a path on the ordered vertices `a — b — c`
 224(MODEL: definitional path shape for a 3-vertex, 2-edge link). -/
 225def IsPathLinkOn (a b c : Fin 6) : Prop :=
 226  a ≠ b ∧ b ≠ c ∧ a ≠ c
 227    ∧ linkVerts = {a, b, c}
 228    ∧ linkEdges = {({a, b} : Finset (Fin 6)), {b, c}}
 229
 230/-- **THEOREM (main witness, path case)**: the link of the hinge triangle
 231`{0,1,2}` in the two-pent complex is a PATH: `4 — 3 — 5`, with the
 232midpoint `3` contributed by the shared tetrahedron.  The hinge is a
 233BOUNDARY hinge: dihedral angles at it form an open angle-sum, not an
 234interior deficit. -/
 235theorem hinge_link_is_path : ∃ a b c : Fin 6, IsPathLinkOn a b c :=
 236  ⟨4, 3, 5, by unfold IsPathLinkOn; decide⟩
 237
 238/-- A cyclic link (MODEL: definitional): a nonempty simple edge set, all
 239edges of size 2, in which EVERY incident vertex has degree exactly 2.
 240This is the combinatorial condition for the link of a triangle to close up
 241around the hinge, making the deficit angle `2π − Σθ` an interior
 242curvature quantity. -/
 243def IsCycleLink {V : Type*} [DecidableEq V] (E : Finset (Finset V)) : Prop :=
 244  E.Nonempty ∧ (∀ e ∈ E, e.card = 2)
 245    ∧ ∀ v : V, (∃ e ∈ E, v ∈ e) → (E.filter (fun e => v ∈ e)).card = 2
 246
 247/-- **THEOREM (counting lemma)**: a cyclic link needs at least 3 edges.
 248Proof: take an edge `e = {a,b}`; degree-2 at `a` gives a second edge
 249`e' ≠ e` through `a`, degree-2 at `b` gives a second edge `e'' ≠ e`
 250through `b`; if `e' = e''` then it contains both `a` and `b`, and having
 251exactly 2 elements it would equal `e` — contradiction.  So `e, e', e''`
 252are three distinct edges. -/
 253theorem cycleLink_three_edges {V : Type*} [DecidableEq V]
 254    (E : Finset (Finset V)) (h : IsCycleLink E) : 3 ≤ E.card := by
 255  obtain ⟨⟨e, he⟩, hcard, hdeg⟩ := h
 256  obtain ⟨a, b, hab, heab⟩ := Finset.card_eq_two.mp (hcard e he)
 257  have ha : a ∈ e := by
 258    rw [heab]; exact Finset.mem_insert_self a {b}
 259  have hb : b ∈ e := by
 260    rw [heab]; exact Finset.mem_insert_of_mem (Finset.mem_singleton_self b)
 261  -- second edge through a
 262  have hdega : 1 < (E.filter (fun f => a ∈ f)).card := by
 263    rw [hdeg a ⟨e, he, ha⟩]; exact one_lt_two
 264  obtain ⟨e', he'mem, he'ne⟩ := Finset.exists_mem_ne hdega e
 265  obtain ⟨he'E, hae'⟩ := Finset.mem_filter.mp he'mem
 266  -- second edge through b
 267  have hdegb : 1 < (E.filter (fun f => b ∈ f)).card := by
 268    rw [hdeg b ⟨e, he, hb⟩]; exact one_lt_two
 269  obtain ⟨e'', he''mem, he''ne⟩ := Finset.exists_mem_ne hdegb e
 270  obtain ⟨he''E, hbe''⟩ := Finset.mem_filter.mp he''mem
 271  -- e' and e'' are distinct: otherwise a common edge ⊇ {a,b} of size 2
 272  -- would equal e
 273  have hne' : e' ≠ e'' := by
 274    intro hEq
 275    have hbe' : b ∈ e' := hEq ▸ hbe''
 276    have hsub : e ⊆ e' := by
 277      rw [heab]
 278      intro x hx
 279      rcases Finset.mem_insert.mp hx with hxa | hxb
 280      · exact hxa ▸ hae'
 281      · exact (Finset.mem_singleton.mp hxb) ▸ hbe'
 282    have heq : e = e' :=
 283      Finset.eq_of_subset_of_card_le hsub
 284        (by rw [hcard e' he'E, hcard e he])
 285    exact he'ne heq.symm
 286  -- three distinct edges inside E
 287  have hnotmem1 : e' ∉ ({e''} : Finset (Finset V)) := by
 288    intro hmem
 289    exact hne' (Finset.mem_singleton.mp hmem)
 290  have hnotmem2 : e ∉ insert e' ({e''} : Finset (Finset V)) := by
 291    intro hmem
 292    rcases Finset.mem_insert.mp hmem with hmem' | hmem''
 293    · exact he'ne hmem'.symm
 294    · exact he''ne (Finset.mem_singleton.mp hmem'').symm
 295  have hsub3 : ({e, e', e''} : Finset (Finset V)) ⊆ E := by
 296    intro f hf
 297    rcases Finset.mem_insert.mp hf with hf1 | hf'
 298    · exact hf1 ▸ he
 299    rcases Finset.mem_insert.mp hf' with hf2 | hf3
 300    · exact hf2 ▸ he'E
 301    · exact (Finset.mem_singleton.mp hf3) ▸ he''E
 302  have hcard3 : ({e, e', e''} : Finset (Finset V)).card = 3 := by
 303    rw [Finset.card_insert_of_notMem hnotmem2,
 304      Finset.card_insert_of_notMem hnotmem1, Finset.card_singleton]
 305  calc 3 = ({e, e', e''} : Finset (Finset V)).card := hcard3.symm
 306    _ ≤ E.card := Finset.card_le_card hsub3
 307
 308/-- **THEOREM (minimal interior-hinge requirement)**: since each pent
 309containing the hinge contributes exactly one link edge (its residual pair
 310`P \ hinge`), a genuine interior hinge — a cyclic link — requires at least
 311THREE 4-simplices around the hinge triangle. -/
 312theorem interior_hinge_needs_three_pents
 313    (pents : Finset (Finset (Fin 6)))
 314    (hcycle : IsCycleLink (pents.image (fun P => P \ hinge))) :
 315    3 ≤ pents.card :=
 316  le_trans (cycleLink_three_edges _ hcycle) Finset.card_image_le
 317
 318/-- **THEOREM (main witness, negative case)**: the two-pent complex can
 319NEVER present the hinge as an interior hinge: its residual link-edge set
 320(2 edges) cannot be a cycle. -/
 321theorem twoPent_hinge_never_interior :
 322    ¬ IsCycleLink (twoPentComplex.image (fun P => P \ hinge)) := by
 323  intro h
 324  have h3 := interior_hinge_needs_three_pents twoPentComplex h
 325  have h2 : twoPentComplex.card = 2 := by decide
 326  omega
 327
 328/-- THEOREM: the hinge link of the two-pent complex is not a cycle (stated
 329directly on `linkEdges` via the residual identification). -/
 330theorem hinge_link_not_cycle : ¬ IsCycleLink linkEdges := by
 331  rw [linkEdges_eq_pent_residues.1]
 332  exact twoPent_hinge_never_interior
 333
 334/-! ## §6. Axiom audit
 335
 336`#print axioms` receipts for the load-bearing witnesses.  Expected output:
 337at most `[propext, Classical.choice, Quot.sound]` (the standard Mathlib
 338trio; no `sorryAx`, no `Lean.ofReduceBool` from `native_decide`, no
 339repo-local axioms). -/
 340
 341#print axioms hinge_link_is_path
 342#print axioms hinge_link_not_cycle
 343#print axioms cycleLink_three_edges
 344#print axioms interior_hinge_needs_three_pents
 345#print axioms twoPent_hinge_never_interior
 346
 347end GluedPentsHingeWitness
 348end SevenGaps
 349end Gravity
 350end IndisputableMonolith
 351