IndisputableMonolith.Geometry.ReggeTriangulation3D

   1import Mathlib.Data.Real.Basic
   2import IndisputableMonolith.Geometry.ReggeRigorousFoundation
   3
   4/-!
   5# Finite 3D Regge Triangulations
   6
   7This module gives the finite incidence scaffold used to lift local
   8tetrahedral identities to arbitrary 3D Regge triangulations.
   9-/
  10
  11namespace IndisputableMonolith
  12namespace Geometry
  13namespace ReggeTriangulation3D
  14
  15open ReggeRigorousFoundation
  16
  17noncomputable section
  18
  19/-- A finite 3D Regge triangulation with abstract incidence data and a
  20nondegenerate squared-edge tuple on every tetrahedron. -/
  21structure Triangulation3D where
  22  nV : ℕ
  23  nE : ℕ
  24  nT : ℕ
  25  edgeVerts : Fin nE → Fin nV × Fin nV
  26  tetVerts : Fin nT → Fin 4 → Fin nV
  27  edgeInTet : Fin nE → Fin nT → Option (Fin 6)
  28  tet : Fin nT → NonDegenerateTet
  29
  30/-- A global edge variation assigns a derivative to each local tetrahedral
  31edge.  This separated representation avoids prematurely choosing a global
  32length-coordinate chart. -/
  33abbrev LocalEdgeVariation (K : Triangulation3D) :=
  34  Fin K.nT → Fin 6 → ℝ
  35
  36end
  37
  38end ReggeTriangulation3D
  39end Geometry
  40end IndisputableMonolith
  41