IndisputableMonolith.Gravity.SevenGaps.SimplicialClass

   1import Mathlib
   2import IndisputableMonolith.Gravity.SevenGaps.PathSumMeasure
   3
   4/-!
   5# Full Theory Phase 0b: the simplicial subclass of the path-sum configuration class
   6
   7## Status: THEOREM (0 sorry, 0 new axiom; `decide` is used only for finite
   8combinatorial checks on the explicit one-tetrahedron witness, no
   9`native_decide`).
  10
  11`SevenGaps.PathSumMeasure.BoundedComplex B` is the garbage-inclusive
  12superclass of bounded incidence configurations: it contains every bounded
  13combinatorial triangulation but also non-simplicial configurations
  14(degenerate edges, repeated vertices in a tetrahedron, multi-edges, tets
  15whose 1-skeleton is missing from the edge list).  This module adds the
  16`IsSimplicial` predicate carving out the true simplicial subclass, proves
  17the predicate decidable, proves the subclass is a `Fintype` with strictly
  18positive cardinality (`simplicialComplex_card_pos`), and exhibits a
  19NON-EMPTY simplicial witness (the single tetrahedron with its full
  201-skeleton, `oneTetComplex`) so positivity does not rest on the vacuous
  21empty complex alone.
  22
  23The simplicial conditions:
  241. no degenerate edges (distinct endpoints);
  252. no multi-edges (edges are injective as unordered vertex pairs);
  263. each tetrahedron has four distinct vertices;
  274. skeleton closure: every vertex pair of every tetrahedron is realized by
  28   an edge of the complex.
  29
  30These four conditions are the combinatorial content of "abstract simplicial
  313-complex presented by its tetrahedra and 1-skeleton" for the incidence
  32shape carried by `BoundedComplex` (vertex/edge/tet lists).  Face (triangle)
  33data is not carried by `BoundedComplex`, so triangle closure is not
  34expressible here; this is honest scope, recorded in
  35`simplicialClassStatus`.
  36-/
  37
  38namespace IndisputableMonolith
  39namespace Gravity
  40namespace SevenGaps
  41namespace PathSumMeasure
  42
  43/-! ## §1. The simplicial predicate -/
  44
  45/-- Unordered-pair equality of ordered vertex pairs. -/
  46def sameUnorderedPair {n : ℕ} (p q : Fin n × Fin n) : Prop :=
  47  p = q ∨ p = q.swap
  48
  49instance {n : ℕ} (p q : Fin n × Fin n) : Decidable (sameUnorderedPair p q) := by
  50  unfold sameUnorderedPair
  51  infer_instance
  52
  53/-- **The simplicial predicate** on a bounded incidence configuration:
  54no degenerate edges, no multi-edges, injective tetrahedron corners, and
  55skeleton closure (every corner pair of every tet is an edge of the
  56complex). -/
  57def IsSimplicial {B : ℕ} (K : BoundedComplex B) : Prop :=
  58  (∀ e : Fin K.nE, (K.edgeVerts e).1 ≠ (K.edgeVerts e).2) ∧
  59  (∀ e e' : Fin K.nE,
  60    sameUnorderedPair (K.edgeVerts e) (K.edgeVerts e') → e = e') ∧
  61  (∀ t : Fin K.nT, Function.Injective (K.tetVerts t)) ∧
  62  (∀ (t : Fin K.nT) (i j : Fin 4), i ≠ j →
  63    ∃ e : Fin K.nE,
  64      sameUnorderedPair (K.edgeVerts e) (K.tetVerts t i, K.tetVerts t j))
  65
  66/-- The simplicial predicate is decidable (all quantifiers range over
  67finite index types). -/
  68instance {B : ℕ} : DecidablePred (IsSimplicial (B := B)) := fun K => by
  69  unfold IsSimplicial
  70  infer_instance
  71
  72/-! ## §2. Finiteness of the simplicial subclass -/
  73
  74/-- The true simplicial subclass of the scoped path-sum configuration
  75class. -/
  76abbrev SimplicialComplex (B : ℕ) : Type :=
  77  {K : BoundedComplex B // IsSimplicial K}
  78
  79/-- **THEOREM (finiteness of the simplicial subclass).**  The simplicial
  80subclass inherits finiteness from the proved finiteness of the superclass
  81(`instFintypeBoundedComplex`) and decidability of the predicate. -/
  82instance instFintypeSimplicialComplex (B : ℕ) : Fintype (SimplicialComplex B) :=
  83  Subtype.fintype _
  84
  85/-- The empty complex is (vacuously) simplicial. -/
  86theorem emptyComplex_isSimplicial (B : ℕ) : IsSimplicial (emptyComplex B) := by
  87  refine ⟨?_, ?_, ?_, ?_⟩
  88  · intro e; exact e.elim0
  89  · intro e; exact e.elim0
  90  · intro t; exact t.elim0
  91  · intro t; exact t.elim0
  92
  93instance (B : ℕ) : Nonempty (SimplicialComplex B) :=
  94  ⟨⟨emptyComplex B, emptyComplex_isSimplicial B⟩⟩
  95
  96/-- **THEOREM (positive count).**  The simplicial subclass is nonempty for
  97every size cap, so the restricted path sum has a nontrivial configuration
  98space. -/
  99theorem simplicialComplex_card_pos (B : ℕ) :
 100    0 < Fintype.card (SimplicialComplex B) :=
 101  Fintype.card_pos
 102
 103/-! ## §3. The non-vacuous witness: a single tetrahedron with full skeleton
 104
 105Positivity via the empty complex alone would be a vacuity risk.  We
 106exhibit the smallest genuinely 3-dimensional simplicial complex: four
 107vertices, six edges (the complete 1-skeleton), one tetrahedron. -/
 108
 109/-- Cap relaxation: a bounded complex at cap `B` is one at any cap
 110`B' ≥ B`, with identical incidence data. -/
 111def relax {B B' : ℕ} (h : B ≤ B') (K : BoundedComplex B) :
 112    BoundedComplex B' where
 113  nV := K.nV
 114  nE := K.nE
 115  nT := K.nT
 116  hV := le_trans K.hV h
 117  hE := le_trans K.hE h
 118  hT := le_trans K.hT h
 119  edgeVerts := K.edgeVerts
 120  tetVerts := K.tetVerts
 121
 122/-- Cap relaxation preserves the simplicial predicate (the predicate reads
 123only the incidence data, which `relax` preserves definitionally). -/
 124theorem relax_isSimplicial {B B' : ℕ} (h : B ≤ B') {K : BoundedComplex B}
 125    (hK : IsSimplicial K) : IsSimplicial (relax h K) :=
 126  hK
 127
 128/-- The six edges of the tetrahedron on four vertices, as ordered pairs
 129(i, j) with i < j. -/
 130def tetEdges : Fin 6 → Fin 4 × Fin 4 :=
 131  ![(0, 1), (0, 2), (0, 3), (1, 2), (1, 3), (2, 3)]
 132
 133/-- The single-tetrahedron complex at the minimal cap: 4 vertices, 6 edges
 134(the complete 1-skeleton), 1 tetrahedron. -/
 135def oneTetComplex : BoundedComplex 6 where
 136  nV := 4
 137  nE := 6
 138  nT := 1
 139  hV := by omega
 140  hE := le_refl 6
 141  hT := by omega
 142  edgeVerts := tetEdges
 143  tetVerts := fun _ i => i
 144
 145/-- **THEOREM (non-vacuous simplicial witness).**  The single-tetrahedron
 146complex is simplicial: distinct edge endpoints, no multi-edges, injective
 147corners, and every corner pair realized by one of the six skeleton edges.
 148Kernel-checked by `decide` on the finite index types (`Fin 4`, `Fin 6`,
 149`Fin 1`); no `native_decide`. -/
 150theorem oneTetComplex_isSimplicial : IsSimplicial oneTetComplex := by
 151  decide
 152
 153/-- **THEOREM.**  Every cap `B ≥ 6` admits a genuinely 3-dimensional
 154simplicial configuration (one tetrahedron, full skeleton): the subclass
 155positivity is not carried by the empty complex alone. -/
 156theorem exists_simplicial_with_tet (B : ℕ) (hB : 6 ≤ B) :
 157    ∃ K : SimplicialComplex B, 0 < K.1.nT :=
 158  ⟨⟨relax hB oneTetComplex, relax_isSimplicial hB oneTetComplex_isSimplicial⟩,
 159    Nat.one_pos⟩
 160
 161/-! ## §4. The restricted path sum -/
 162
 163/-- The path sum restricted to the simplicial subclass, with the same
 164`1/|Aut|` measure and weight as `Z`. -/
 165noncomputable def Zsimp (B : ℕ) (w : BoundedComplex B → ℂ) : ℂ :=
 166  ∑ K : SimplicialComplex B, (mu K.1 : ℂ) * w K.1
 167
 168/-- **THEOREM (UV-finiteness of the simplicial path sum).**  For unit-modulus
 169weights the restricted path sum is bounded by the simplicial configuration
 170count. -/
 171theorem Zsimp_norm_le_card (B : ℕ) (w : BoundedComplex B → ℂ)
 172    (hw : ∀ K, ‖w K‖ ≤ 1) :
 173    ‖Zsimp B w‖ ≤ (Fintype.card (SimplicialComplex B) : ℝ) := by
 174  unfold Zsimp
 175  calc ‖∑ K : SimplicialComplex B, (mu K.1 : ℂ) * w K.1‖
 176      ≤ ∑ K : SimplicialComplex B, ‖(mu K.1 : ℂ) * w K.1‖ := norm_sum_le _ _
 177    _ ≤ ∑ _K : SimplicialComplex B, (1 : ℝ) := by
 178        refine Finset.sum_le_sum fun K _ => ?_
 179        rw [norm_mul, Complex.norm_real, Real.norm_eq_abs,
 180          abs_of_pos (mu_pos K.1)]
 181        calc mu K.1 * ‖w K.1‖
 182            ≤ 1 * 1 := mul_le_mul (mu_le_one K.1) (hw K.1)
 183              (norm_nonneg _) zero_le_one
 184          _ = 1 := one_mul 1
 185    _ = (Fintype.card (SimplicialComplex B) : ℝ) := by
 186        rw [Finset.sum_const, Finset.card_univ, nsmul_eq_mul, mul_one]
 187
 188/-! ## §5. Status ledger -/
 189
 190/-- Status of the simplicial-subclass repair (Phase 0b).  Honest scope:
 191`BoundedComplex` carries no triangle (2-face) list, so triangle closure is
 192not expressible in this incidence shape; the four proved conditions are the
 193full simplicial content available at this shape. -/
 194structure SimplicialClassStatus where
 195  simplicial_predicate_decidable : Bool
 196  subclass_fintype_proved : Bool
 197  subclass_card_pos_proved : Bool
 198  nonvacuous_witness_constructed : Bool
 199  triangle_closure_expressible : Bool
 200
 201/-- The Phase-0b status record. -/
 202def simplicialClassStatus : SimplicialClassStatus where
 203  simplicial_predicate_decidable := true
 204  subclass_fintype_proved := true
 205  subclass_card_pos_proved := true
 206  nonvacuous_witness_constructed := true
 207  triangle_closure_expressible := false
 208
 209/-- Status flags (rfl-forced). -/
 210theorem simplicialClassStatus_flags :
 211    simplicialClassStatus.simplicial_predicate_decidable = true ∧
 212    simplicialClassStatus.subclass_fintype_proved = true ∧
 213    simplicialClassStatus.subclass_card_pos_proved = true ∧
 214    simplicialClassStatus.nonvacuous_witness_constructed = true ∧
 215    simplicialClassStatus.triangle_closure_expressible = false :=
 216  ⟨rfl, rfl, rfl, rfl, rfl⟩
 217
 218end PathSumMeasure
 219end SevenGaps
 220end Gravity
 221end IndisputableMonolith
 222