IndisputableMonolith.Geometry.FreudenthalCubeTriangulation

   1import IndisputableMonolith.Geometry.ReggeActionFirstVariation
   2
   3/-!
   4# Freudenthal Six-Tetrahedron Cube Triangulation
   5
   6This module instantiates the incidence bookkeeping class for the standard
   7Freudenthal decomposition of one unit cube into six tetrahedra, using the
   8body diagonal from vertex `0` to vertex `7`.
   9
  10Cube vertex labels are binary coordinates:
  11
  12* `0 = (0,0,0)`
  13* `1 = (1,0,0)`
  14* `2 = (0,1,0)`
  15* `3 = (1,1,0)`
  16* `4 = (0,0,1)`
  17* `5 = (1,0,1)`
  18* `6 = (0,1,1)`
  19* `7 = (1,1,1)`
  20
  21The six tetrahedra are the monotone paths from `0` to `7`.
  22-/
  23
  24namespace IndisputableMonolith
  25namespace Geometry
  26namespace FreudenthalCubeTriangulation
  27
  28open ReggeRigorousFoundation
  29open ReggeTriangulation3D
  30open Triangulation3DConsistency
  31open ReggeActionFirstVariation
  32open SchlaefliTetrahedronProof
  33
  34noncomputable section
  35
  36/-- The local squared-edge tuple for every Freudenthal tetrahedron in the unit
  37cube: three unit step edges, two face diagonals, and one body diagonal. -/
  38def freudenthalTetSqEdges : CayleyMengerPolynomial.SqEdges
  39  | 0 => 1
  40  | 1 => 2
  41  | 2 => 3
  42  | 3 => 1
  43  | 4 => 2
  44  | 5 => 1
  45
  46theorem cm3_freudenthalTetSqEdges :
  47    CayleyMengerPolynomial.cm3 freudenthalTetSqEdges = 8 := by
  48  unfold freudenthalTetSqEdges CayleyMengerPolynomial.cm3
  49  norm_num
  50
  51/-- A unit-cube Freudenthal tetrahedron is nondegenerate. -/
  52def freudenthalTet : NonDegenerateTet where
  53  sqEdge := freudenthalTetSqEdges
  54  sqEdge_pos := by
  55    intro i
  56    fin_cases i <;> norm_num [freudenthalTetSqEdges]
  57  cm_pos := by
  58    rw [cm3_freudenthalTetSqEdges]
  59    norm_num
  60
  61/-- The 19 unique edges in the Freudenthal triangulation of the unit cube. -/
  62def edgeVerts : Fin 19 → Fin 8 × Fin 8
  63  | 0 => (0, 1)
  64  | 1 => (0, 2)
  65  | 2 => (0, 4)
  66  | 3 => (0, 3)
  67  | 4 => (0, 5)
  68  | 5 => (0, 6)
  69  | 6 => (0, 7)
  70  | 7 => (1, 3)
  71  | 8 => (1, 5)
  72  | 9 => (1, 7)
  73  | 10 => (2, 3)
  74  | 11 => (2, 6)
  75  | 12 => (2, 7)
  76  | 13 => (3, 7)
  77  | 14 => (4, 5)
  78  | 15 => (4, 6)
  79  | 16 => (4, 7)
  80  | 17 => (5, 7)
  81  | 18 => (6, 7)
  82  | ⟨n+19, h⟩ => absurd h (by omega)
  83
  84/-- Squared length of each global edge. -/
  85def globalSqEdge : Fin 19 → ℝ
  86  | 0 => 1
  87  | 1 => 1
  88  | 2 => 1
  89  | 3 => 2
  90  | 4 => 2
  91  | 5 => 2
  92  | 6 => 3
  93  | 7 => 1
  94  | 8 => 1
  95  | 9 => 2
  96  | 10 => 1
  97  | 11 => 1
  98  | 12 => 2
  99  | 13 => 1
 100  | 14 => 1
 101  | 15 => 1
 102  | 16 => 2
 103  | 17 => 1
 104  | 18 => 1
 105  | ⟨n+19, h⟩ => absurd h (by omega)
 106
 107/-- The six tetrahedra as vertex lists. -/
 108def tetVerts : Fin 6 → Fin 4 → Fin 8
 109  | 0, 0 => 0
 110  | 0, 1 => 1
 111  | 0, 2 => 3
 112  | 0, 3 => 7
 113  | 1, 0 => 0
 114  | 1, 1 => 1
 115  | 1, 2 => 5
 116  | 1, 3 => 7
 117  | 2, 0 => 0
 118  | 2, 1 => 2
 119  | 2, 2 => 3
 120  | 2, 3 => 7
 121  | 3, 0 => 0
 122  | 3, 1 => 2
 123  | 3, 2 => 6
 124  | 3, 3 => 7
 125  | 4, 0 => 0
 126  | 4, 1 => 4
 127  | 4, 2 => 5
 128  | 4, 3 => 7
 129  | 5, 0 => 0
 130  | 5, 1 => 4
 131  | 5, 2 => 6
 132  | 5, 3 => 7
 133
 134/-- Chosen global edge for each local tetrahedral edge slot. -/
 135def localEdgeOf : Fin 6 → Fin 6 → Fin 19
 136  | 0, 0 => 0
 137  | 0, 1 => 3
 138  | 0, 2 => 6
 139  | 0, 3 => 7
 140  | 0, 4 => 9
 141  | 0, 5 => 13
 142  | 1, 0 => 0
 143  | 1, 1 => 4
 144  | 1, 2 => 6
 145  | 1, 3 => 8
 146  | 1, 4 => 9
 147  | 1, 5 => 17
 148  | 2, 0 => 1
 149  | 2, 1 => 3
 150  | 2, 2 => 6
 151  | 2, 3 => 10
 152  | 2, 4 => 12
 153  | 2, 5 => 13
 154  | 3, 0 => 1
 155  | 3, 1 => 5
 156  | 3, 2 => 6
 157  | 3, 3 => 11
 158  | 3, 4 => 12
 159  | 3, 5 => 18
 160  | 4, 0 => 2
 161  | 4, 1 => 4
 162  | 4, 2 => 6
 163  | 4, 3 => 14
 164  | 4, 4 => 16
 165  | 4, 5 => 17
 166  | 5, 0 => 2
 167  | 5, 1 => 5
 168  | 5, 2 => 6
 169  | 5, 3 => 15
 170  | 5, 4 => 16
 171  | 5, 5 => 18
 172
 173/-- Incidence map from a global edge and tetrahedron to the local edge slot,
 174if the edge belongs to that tetrahedron. -/
 175def edgeInTet : Fin 19 → Fin 6 → Option (Fin 6)
 176  | 0, 0 => some 0
 177  | 3, 0 => some 1
 178  | 6, 0 => some 2
 179  | 7, 0 => some 3
 180  | 9, 0 => some 4
 181  | 13, 0 => some 5
 182  | 0, 1 => some 0
 183  | 4, 1 => some 1
 184  | 6, 1 => some 2
 185  | 8, 1 => some 3
 186  | 9, 1 => some 4
 187  | 17, 1 => some 5
 188  | 1, 2 => some 0
 189  | 3, 2 => some 1
 190  | 6, 2 => some 2
 191  | 10, 2 => some 3
 192  | 12, 2 => some 4
 193  | 13, 2 => some 5
 194  | 1, 3 => some 0
 195  | 5, 3 => some 1
 196  | 6, 3 => some 2
 197  | 11, 3 => some 3
 198  | 12, 3 => some 4
 199  | 18, 3 => some 5
 200  | 2, 4 => some 0
 201  | 4, 4 => some 1
 202  | 6, 4 => some 2
 203  | 14, 4 => some 3
 204  | 16, 4 => some 4
 205  | 17, 4 => some 5
 206  | 2, 5 => some 0
 207  | 5, 5 => some 1
 208  | 6, 5 => some 2
 209  | 15, 5 => some 3
 210  | 16, 5 => some 4
 211  | 18, 5 => some 5
 212  | _, _ => none
 213
 214/-- The finite Freudenthal cube triangulation. -/
 215def freudenthalCube : Triangulation3D where
 216  nV := 8
 217  nE := 19
 218  nT := 6
 219  edgeVerts := edgeVerts
 220  tetVerts := tetVerts
 221  edgeInTet := edgeInTet
 222  tet := fun _ => freudenthalTet
 223
 224theorem edgeInTet_iff_localEdgeOf
 225    (e : Fin 19) (τ f : Fin 6) :
 226    edgeInTet e τ = some f ↔ e = localEdgeOf τ f := by
 227  fin_cases e <;> fin_cases τ <;> fin_cases f <;>
 228    simp [edgeInTet, localEdgeOf]
 229
 230theorem local_sqEdge_eq_global
 231    (e : Fin 19) (τ f : Fin 6) (h : edgeInTet e τ = some f) :
 232    freudenthalTet.sqEdge f = globalSqEdge e := by
 233  fin_cases e <;> fin_cases τ <;> fin_cases f <;>
 234    simp [edgeInTet, freudenthalTet, freudenthalTetSqEdges, globalSqEdge] at h ⊢
 235
 236theorem edgeInTet_vertices
 237    (e : Fin 19) (τ f : Fin 6) (h : edgeInTet e τ = some f) :
 238      let ev := edgeVerts e
 239      let tv := ReggeRigorousFoundation.edgeVertices f
 240      (tetVerts τ tv.1 = ev.1 ∧ tetVerts τ tv.2 = ev.2) ∨
 241        (tetVerts τ tv.1 = ev.2 ∧ tetVerts τ tv.2 = ev.1) := by
 242  fin_cases e <;> fin_cases τ <;> fin_cases f <;>
 243    simp [edgeInTet, edgeVerts, tetVerts, ReggeRigorousFoundation.edgeVertices] at h ⊢
 244
 245theorem localEdge_complete (τ f : Fin 6) :
 246    ∃ e : Fin 19, edgeInTet e τ = some f := by
 247  exact ⟨localEdgeOf τ f, (edgeInTet_iff_localEdgeOf (localEdgeOf τ f) τ f).2 rfl⟩
 248
 249/-- Incidence consistency for the Freudenthal cube. -/
 250def freudenthalCube_incidenceConsistent :
 251    IncidenceConsistent freudenthalCube where
 252  globalSqEdge := globalSqEdge
 253  edgeInTet_vertices := by
 254    intro e τ f h
 255    exact edgeInTet_vertices e τ f h
 256  local_sqEdge_eq_global := by
 257    intro e τ f h
 258    exact local_sqEdge_eq_global e τ f h
 259  localEdge_complete := by
 260    intro τ f
 261    exact localEdge_complete τ f
 262  local_schlaefli := by
 263    intro τ
 264    exact schlaefliTetrahedronClosedForm freudenthalTet
 265
 266/-- The Freudenthal cube has the intended unique/no-duplication local edge-slot
 267partition. -/
 268def freudenthalCube_edgeSlotPartition :
 269    IncidenceEdgeSlotPartition freudenthalCube freudenthalCube_incidenceConsistent where
 270  localEdgeOf := localEdgeOf
 271  edgeInTet_iff := by
 272    intro e τ f
 273    exact edgeInTet_iff_localEdgeOf e τ f
 274
 275/-- Concrete edge-slot bookkeeping for the Freudenthal six-tetrahedron cube. -/
 276def freudenthalCube_edgeSlotBookkeeping :
 277    IncidenceEdgeSlotBookkeeping freudenthalCube freudenthalCube_incidenceConsistent :=
 278  incidenceEdgeSlotBookkeeping_of_partition
 279    freudenthalCube freudenthalCube_incidenceConsistent freudenthalCube_edgeSlotPartition
 280
 281end
 282
 283end FreudenthalCubeTriangulation
 284end Geometry
 285end IndisputableMonolith
 286