IndisputableMonolith.Geometry.Triangulation3DConsistency

   1import IndisputableMonolith.Geometry.SchlaefliTriangulation3D
   2import IndisputableMonolith.Geometry.SchlaefliTetrahedronProof
   3
   4/-!
   5# Incidence-Consistent 3D Regge Triangulations
   6
   7This module strengthens the abstract `Triangulation3D` scaffold with the
   8incidence and local-Schläfli data needed to construct global Schläfli
   9cancellation.
  10-/
  11
  12namespace IndisputableMonolith
  13namespace Geometry
  14namespace Triangulation3DConsistency
  15
  16open ReggeTriangulation3D
  17open SchlaefliTriangulation3D
  18open SchlaefliTetrahedron
  19open SchlaefliTetrahedronProof
  20
  21noncomputable section
  22
  23/-- Strong incidence consistency for the current 3D Regge scaffold.
  24
  25The first fields state that local tetrahedral edge slots agree with global
  26edge endpoints up to orientation.  The last field is the local closed-form
  27Schläfli proof required to build global Schläfli without caller-supplied
  28`TriangulationSchlaefliData`. -/
  29structure IncidenceConsistent (K : Triangulation3D) where
  30  globalSqEdge : Fin K.nE → ℝ
  31  edgeInTet_vertices :
  32    ∀ e τ f, K.edgeInTet e τ = some f →
  33      let ev := K.edgeVerts e
  34      let tv := ReggeRigorousFoundation.edgeVertices f
  35      (K.tetVerts τ tv.1 = ev.1 ∧ K.tetVerts τ tv.2 = ev.2) ∨
  36        (K.tetVerts τ tv.1 = ev.2 ∧ K.tetVerts τ tv.2 = ev.1)
  37  local_sqEdge_eq_global :
  38    ∀ e τ f, K.edgeInTet e τ = some f →
  39      (K.tet τ).sqEdge f = globalSqEdge e
  40  localEdge_complete :
  41    ∀ τ f, ∃ e : Fin K.nE, K.edgeInTet e τ = some f
  42  local_schlaefli :
  43    ∀ τ : Fin K.nT, TetraSchlaefliClosedEquation (K.tet τ)
  44
  45/-- Pure geometric incidence consistency, without storing local Schläfli
  46proofs as fields.  This is the right input once the tetrahedral Schläfli
  47theorem is available globally. -/
  48structure IncidenceGeometry (K : Triangulation3D) where
  49  globalSqEdge : Fin K.nE → ℝ
  50  edgeInTet_vertices :
  51    ∀ e τ f, K.edgeInTet e τ = some f →
  52      let ev := K.edgeVerts e
  53      let tv := ReggeRigorousFoundation.edgeVertices f
  54      (K.tetVerts τ tv.1 = ev.1 ∧ K.tetVerts τ tv.2 = ev.2) ∨
  55        (K.tetVerts τ tv.1 = ev.2 ∧ K.tetVerts τ tv.2 = ev.1)
  56  local_sqEdge_eq_global :
  57    ∀ e τ f, K.edgeInTet e τ = some f →
  58      (K.tet τ).sqEdge f = globalSqEdge e
  59  localEdge_complete :
  60    ∀ τ f, ∃ e : Fin K.nE, K.edgeInTet e τ = some f
  61
  62/-- A global edge length from the incidence-level squared-edge chart. -/
  63def globalEdgeLength (K : Triangulation3D) (hK : IncidenceConsistent K)
  64    (e : Fin K.nE) : ℝ :=
  65  Real.sqrt (hK.globalSqEdge e)
  66
  67/-- Local tetrahedral squared-edge slots agree with the global squared-edge
  68chart whenever the incidence map identifies them. -/
  69theorem localSqEdge_eq_globalSqEdge
  70    (K : Triangulation3D) (hK : IncidenceConsistent K)
  71    (e : Fin K.nE) (τ : Fin K.nT) (f : Fin 6)
  72    (h : K.edgeInTet e τ = some f) :
  73    (K.tet τ).sqEdge f = hK.globalSqEdge e :=
  74  hK.local_sqEdge_eq_global e τ f h
  75
  76/-- The local edge length at any incident tetrahedral edge equals the global
  77edge length determined by the consistency chart. -/
  78theorem localEdgeLength_eq_globalEdgeLength
  79    (K : Triangulation3D) (hK : IncidenceConsistent K)
  80    (e : Fin K.nE) (τ : Fin K.nT) (f : Fin 6)
  81    (h : K.edgeInTet e τ = some f) :
  82    Real.sqrt ((K.tet τ).sqEdge f) = globalEdgeLength K hK e := by
  83  unfold globalEdgeLength
  84  rw [localSqEdge_eq_globalSqEdge K hK e τ f h]
  85
  86/-- Construct local Schläfli data on every tetrahedron from the incidence
  87mixin's closed-form local Schläfli proof. -/
  88def triangulationSchlaefliData_of_incidence
  89    (K : Triangulation3D) (hK : IncidenceConsistent K) :
  90    TriangulationSchlaefliData K where
  91  tetData := fun τ =>
  92    tetraSchlaefliDerivativeData_closedForm (K.tet τ) (hK.local_schlaefli τ)
  93
  94/-- Strong incidence plus local closed-form Schläfli gives global Schläfli. -/
  95theorem global_schlaefli_from_incidence
  96    (K : Triangulation3D) (hK : IncidenceConsistent K) (e' : Fin 6) :
  97    globalSchlaefliLHS K (triangulationSchlaefliData_of_incidence K hK) e' =
  98      globalSchlaefliRHS K (triangulationSchlaefliData_of_incidence K hK) e' :=
  99  global_schlaefli_of_local K (triangulationSchlaefliData_of_incidence K hK) e'
 100
 101/-- Incidence consistency constructs the global Schläfli data package. -/
 102theorem nonempty_triangulationSchlaefliData_of_incidence
 103    (K : Triangulation3D) (hK : IncidenceConsistent K) :
 104    Nonempty (TriangulationSchlaefliData K) :=
 105  ⟨triangulationSchlaefliData_of_incidence K hK⟩
 106
 107/-- Once the local closed-form Schläfli theorem is proved globally, pure
 108incidence geometry constructs local Schläfli data on every tetrahedron with
 109no stored local Schläfli field. -/
 110def triangulationSchlaefliData_of_geometry
 111    (K : Triangulation3D) (_hK : IncidenceGeometry K)
 112    (hLocal : SchlaefliTetrahedronClosedFormTarget) :
 113    TriangulationSchlaefliData K where
 114  tetData := fun τ =>
 115    tetraSchlaefliDerivativeData_closedForm (K.tet τ) (hLocal (K.tet τ))
 116
 117/-- Pure incidence geometry plus the local theorem gives global Schläfli. -/
 118theorem global_schlaefli_from_geometry
 119    (K : Triangulation3D) (hK : IncidenceGeometry K)
 120    (hLocal : SchlaefliTetrahedronClosedFormTarget) (e' : Fin 6) :
 121    globalSchlaefliLHS K (triangulationSchlaefliData_of_geometry K hK hLocal) e' =
 122      globalSchlaefliRHS K (triangulationSchlaefliData_of_geometry K hK hLocal) e' :=
 123  global_schlaefli_of_local K (triangulationSchlaefliData_of_geometry K hK hLocal) e'
 124
 125end
 126
 127end Triangulation3DConsistency
 128end Geometry
 129end IndisputableMonolith
 130