IndisputableMonolith.Gravity.SevenGaps.ThreePentInteriorHingeWitness

   1import IndisputableMonolith.Gravity.SevenGaps.GluedPentsHingeWitness
   2
   3/-!
   4# Three-Pent Interior Hinge Witness: the minimal cyclic hinge link
   5
   6Panel P1-remainder live bet C12; witness gates whether glued-pent expressions
   7may be called Regge action.  This module supplies the POSITIVE half of the
   8gate: the minimal complex whose hinge link IS a cycle, complementing the
   9committed two-pent path witness (`GluedPentsHingeWitness`, whose counting
  10lemma `interior_hinge_needs_three_pents` proves three pents are necessary).
  11
  12## The complex
  13
  14Three 4-simplices ("pents") on the vertex set `Fin 6`, all containing the
  15hinge triangle `hinge = {0,1,2}` (imported from the two-pent module):
  16
  17* `pentA = {0,1,2,3,4}` (residual pair `{3,4}`),
  18* `pentB = {0,1,2,4,5}` (residual pair `{4,5}`),
  19* `pentC = {0,1,2,3,5}` (residual pair `{3,5}`).
  20
  21The gluing is face-to-face: each adjacent pair of pents shares EXACTLY ONE
  22tetrahedron of 4 vertices containing the hinge
  23(`A ∩ B = {0,1,2,4}`, `B ∩ C = {0,1,2,5}`, `A ∩ C = {0,1,2,3}`;
  24`pairwise_shared_tets`, `pairwise_shared_tets_unique`), and the triple
  25intersection is exactly the hinge triangle (`triple_intersection`).
  26
  27## What is proved (kernel `decide` + structural composition)
  28
  29* each pent contributes exactly one residual link edge
  30  (`residual_edges`, `linkEdges_eq_pent_residues`);
  31* the hinge link has vertex set `{3,4,5}` and edge set
  32  `{{3,4},{4,5},{3,5}}` — the triangle cycle `3 — 4 — 5 — 3`
  33  (`linkVerts_eq`, `linkEdges_eq`);
  34* every link vertex has degree exactly 2 (`linkDegrees`);
  35* **`threePent_hinge_is_interior`**: the link-edge set satisfies
  36  `IsCycleLink` (imported cyclic-link predicate) — the hinge `{0,1,2}` is
  37  a GENUINE INTERIOR hinge of the three-pent complex;
  38* **`hinge_link_is_cycle`**: the same statement on the module's own
  39  `linkEdges` via the residual identification;
  40* **`threePent_minimality`**: this complex has exactly 3 pents and, by the
  41  committed counting lemma, ANY complex presenting the hinge as interior
  42  has at least 3 — so this is THE minimal interior-hinge configuration
  43  (the lower bound is attained).
  44
  45## Honest scope (do-not-overclaim clause)
  46
  47MODEL data, THEOREM incidence facts, combinatorial only.  This witness
  48licenses calling a deficit `2π − Σθ` at this hinge an interior curvature
  49quantity AT THE INCIDENCE LEVEL: the dihedral angles around the hinge
  50close up in a cycle, so their sum is compared against a full turn, which
  51is exactly what "Regge action at an interior hinge" requires
  52combinatorially.  It does NOT by itself provide edge-length or
  53causal-structure consistency for three glued CAUSAL pents (consistent
  54(4,1)/(3,2) edge-length assignments around the cycle, and the resulting
  55angle values): that metric compatibility question remains OPEN and is a
  56separate lane.
  57
  58## Honesty tiers
  59
  60* THEOREM: every declared theorem below; zero sorry, zero admit, zero new
  61  axioms; finite incidence facts kernel-checked by `decide`
  62  (no `native_decide`); the minimality bound composes the committed
  63  structural lemma `interior_hinge_needs_three_pents`.
  64* MODEL: `pentA`, `pentB`, `pentC`, `threePentComplex`, `tets`,
  65  `linkVerts`, `linkEdges`, `linkDegree` are definitional encodings
  66  (simplices as `Finset (Fin 6)`), mirroring the committed two-pent
  67  module's representation with the hinge `{0,1,2}` shared literally.
  68-/
  69
  70namespace IndisputableMonolith
  71namespace Gravity
  72namespace SevenGaps
  73namespace ThreePentInteriorHingeWitness
  74
  75open Finset
  76open GluedPentsHingeWitness (hinge IsCycleLink cycleLink_three_edges
  77  interior_hinge_needs_three_pents)
  78
  79/-! ## §1. The three-pent complex (MODEL: concrete combinatorial data) -/
  80
  81/-- First pent: vertices `{0,1,2,3,4}`, residual pair `{3,4}`. -/
  82def pentA : Finset (Fin 6) := {0, 1, 2, 3, 4}
  83
  84/-- Second pent: vertices `{0,1,2,4,5}`, residual pair `{4,5}`. -/
  85def pentB : Finset (Fin 6) := {0, 1, 2, 4, 5}
  86
  87/-- Third pent: vertices `{0,1,2,3,5}`, residual pair `{3,5}`. -/
  88def pentC : Finset (Fin 6) := {0, 1, 2, 3, 5}
  89
  90/-- The three-pent complex, presented by its maximal simplices. -/
  91def threePentComplex : Finset (Finset (Fin 6)) := {pentA, pentB, pentC}
  92
  93/-- All tetrahedra (3-faces) of the complex: the 4-element subsets of the
  94pents. -/
  95def tets : Finset (Finset (Fin 6)) :=
  96  threePentComplex.biUnion (Finset.powersetCard 4)
  97
  98/-- Link vertices of the hinge: vertices `v ∉ hinge` with
  99`hinge ∪ {v}` a tetrahedron of the complex. -/
 100def linkVerts : Finset (Fin 6) :=
 101  Finset.univ.filter (fun v => v ∉ hinge ∧ insert v hinge ∈ tets)
 102
 103/-- Link edges of the hinge: vertex pairs `E` disjoint from the hinge with
 104`hinge ∪ E` a pent of the complex (same definition shape as the committed
 105two-pent module, adapted to `threePentComplex`). -/
 106def linkEdges : Finset (Finset (Fin 6)) :=
 107  (Finset.univ.powersetCard 2).filter
 108    (fun E => E ∩ hinge = ∅ ∧ hinge ∪ E ∈ threePentComplex)
 109
 110/-- Degree of a vertex in the link graph of the hinge. -/
 111def linkDegree (v : Fin 6) : ℕ :=
 112  (linkEdges.filter (fun e => v ∈ e)).card
 113
 114/-! ## §2. Face-to-face gluing data (THEOREM, kernel `decide`) -/
 115
 116/-- THEOREM (by `decide`): all three pents are genuine 4-simplices
 117(5 distinct vertices each) and are pairwise distinct, and each contains
 118the hinge. -/
 119theorem pents_are_distinct_foursimplices :
 120    pentA.card = 5 ∧ pentB.card = 5 ∧ pentC.card = 5
 121      ∧ pentA ≠ pentB ∧ pentB ≠ pentC ∧ pentA ≠ pentC
 122      ∧ hinge ⊆ pentA ∧ hinge ⊆ pentB ∧ hinge ⊆ pentC := by decide
 123
 124/-- THEOREM (by `decide`): each adjacent pair of pents intersects in a
 125tetrahedron (4 vertices) containing the hinge — the gluing is
 126face-to-face around the hinge. -/
 127theorem pairwise_shared_tets :
 128    (pentA ∩ pentB = ({0, 1, 2, 4} : Finset (Fin 6))
 129        ∧ (pentA ∩ pentB).card = 4 ∧ hinge ⊆ pentA ∩ pentB)
 130      ∧ (pentB ∩ pentC = ({0, 1, 2, 5} : Finset (Fin 6))
 131        ∧ (pentB ∩ pentC).card = 4 ∧ hinge ⊆ pentB ∩ pentC)
 132      ∧ (pentA ∩ pentC = ({0, 1, 2, 3} : Finset (Fin 6))
 133        ∧ (pentA ∩ pentC).card = 4 ∧ hinge ⊆ pentA ∩ pentC) := by decide
 134
 135/-- THEOREM (by `decide`): each pair of pents shares EXACTLY ONE
 136tetrahedral face (the intersection of their 4-element subset families is
 137a singleton). -/
 138theorem pairwise_shared_tets_unique :
 139    Finset.powersetCard 4 pentA ∩ Finset.powersetCard 4 pentB
 140        = {({0, 1, 2, 4} : Finset (Fin 6))}
 141      ∧ Finset.powersetCard 4 pentB ∩ Finset.powersetCard 4 pentC
 142        = {({0, 1, 2, 5} : Finset (Fin 6))}
 143      ∧ Finset.powersetCard 4 pentA ∩ Finset.powersetCard 4 pentC
 144        = {({0, 1, 2, 3} : Finset (Fin 6))} := by decide
 145
 146/-- THEOREM (by `decide`): the triple intersection of the three pents is
 147exactly the hinge triangle — the three pents wrap around the hinge and
 148nothing more. -/
 149theorem triple_intersection : pentA ∩ pentB ∩ pentC = hinge := by decide
 150
 151/-! ## §3. The hinge link: the triangle cycle (THEOREM, kernel `decide`) -/
 152
 153/-- THEOREM (by `decide`): each pent contributes exactly one residual link
 154edge. -/
 155theorem residual_edges :
 156    pentA \ hinge = ({3, 4} : Finset (Fin 6))
 157      ∧ pentB \ hinge = ({4, 5} : Finset (Fin 6))
 158      ∧ pentC \ hinge = ({3, 5} : Finset (Fin 6)) := by decide
 159
 160/-- THEOREM (by `decide`): the link of the hinge has vertex set
 161`{3, 4, 5}`. -/
 162theorem linkVerts_eq : linkVerts = {3, 4, 5} := by decide
 163
 164/-- THEOREM (by `decide`): the link of the hinge has edge set
 165`{{3,4}, {4,5}, {3,5}}` — the triangle cycle `3 — 4 — 5 — 3` — with one
 166edge per pent, three edges in total. -/
 167theorem linkEdges_eq :
 168    linkEdges = {({3, 4} : Finset (Fin 6)), {4, 5}, {3, 5}}
 169      ∧ linkEdges.card = 3 := by decide
 170
 171/-- THEOREM (by `decide`): the link edges are exactly the residual pairs
 172`P \ hinge` of the pents. -/
 173theorem linkEdges_eq_pent_residues :
 174    linkEdges = threePentComplex.image (fun P => P \ hinge) := by decide
 175
 176/-- THEOREM (by `decide`): every link vertex has degree exactly 2 — the
 177closed-chain condition a boundary hinge fails (the two-pent path witness
 178had endpoint degrees 1). -/
 179theorem linkDegrees :
 180    linkDegree 3 = 2 ∧ linkDegree 4 = 2 ∧ linkDegree 5 = 2 := by decide
 181
 182/-! ## §4. The headline: genuine interior hinge, and minimality -/
 183
 184/-- **THEOREM (main witness, cycle case)**: the residual link-edge set of
 185the three-pent complex satisfies `IsCycleLink` — the hinge `{0,1,2}` is a
 186GENUINE INTERIOR hinge.  At the incidence level this is exactly what a
 187Regge deficit `2π − Σθ` at the hinge requires: the dihedral angles close
 188up in a cycle around the hinge. -/
 189theorem threePent_hinge_is_interior :
 190    IsCycleLink (threePentComplex.image (fun P => P \ hinge)) := by
 191  unfold IsCycleLink
 192  decide
 193
 194/-- THEOREM: the same statement on this module's `linkEdges`, via the
 195residual identification. -/
 196theorem hinge_link_is_cycle : IsCycleLink linkEdges := by
 197  rw [linkEdges_eq_pent_residues]
 198  exact threePent_hinge_is_interior
 199
 200/-- **THEOREM (minimality)**: the three-pent complex attains the proved
 201lower bound: it has exactly 3 pents, and by the committed counting lemma
 202(`interior_hinge_needs_three_pents`) ANY family of pents presenting the
 203hinge as interior has at least 3.  This is THE minimal interior-hinge
 204configuration. -/
 205theorem threePent_minimality :
 206    threePentComplex.card = 3
 207      ∧ (∀ pents : Finset (Finset (Fin 6)),
 208          IsCycleLink (pents.image (fun P => P \ hinge)) → 3 ≤ pents.card) :=
 209  ⟨by decide, fun pents h => interior_hinge_needs_three_pents pents h⟩
 210
 211/-! ## §5. Axiom audit
 212
 213`#print axioms` receipts for the load-bearing witnesses.  Expected output:
 214at most `[propext, Classical.choice, Quot.sound]` (the standard Mathlib
 215trio; no `sorryAx`, no `Lean.ofReduceBool` from `native_decide`, no
 216repo-local axioms). -/
 217
 218#print axioms threePent_hinge_is_interior
 219#print axioms hinge_link_is_cycle
 220#print axioms threePent_minimality
 221#print axioms linkEdges_eq
 222#print axioms linkDegrees
 223
 224end ThreePentInteriorHingeWitness
 225end SevenGaps
 226end Gravity
 227end IndisputableMonolith
 228