IndisputableMonolith.Geometry.FreudenthalTwoCubeStrip

   1import IndisputableMonolith.Geometry.FreudenthalCubeTriangulation
   2
   3/-!
   4# Two-Cube Freudenthal Strip
   5
   6This module gives the smallest nontrivial multi-cube Freudenthal example:
   7two unit cubes sharing one square face, each decomposed into six Freudenthal
   8tetrahedra with compatible face triangulation.
   9
  10It proves the global local-edge-slot partition after deduplicating the five
  11shared face edges.  This is the first concrete multi-cube incidence instance
  12beyond the one-cube sanity check.
  13-/
  14
  15namespace IndisputableMonolith
  16namespace Geometry
  17namespace FreudenthalTwoCubeStrip
  18
  19open ReggeRigorousFoundation
  20open ReggeTriangulation3D
  21open Triangulation3DConsistency
  22open ReggeActionFirstVariation
  23open SchlaefliTetrahedronProof
  24
  25noncomputable section
  26
  27abbrev V := Fin 12
  28abbrev E := Fin 33
  29abbrev T := Fin 12
  30
  31/-- The 33 unique global edges in the two-cube Freudenthal strip. -/
  32def edgeVerts : E → V × V
  33  | 0 => (0, 1)
  34  | 1 => (0, 3)
  35  | 2 => (0, 6)
  36  | 3 => (0, 4)
  37  | 4 => (0, 7)
  38  | 5 => (0, 9)
  39  | 6 => (0, 10)
  40  | 7 => (1, 4)
  41  | 8 => (1, 7)
  42  | 9 => (1, 10)
  43  | 10 => (3, 4)
  44  | 11 => (3, 9)
  45  | 12 => (3, 10)
  46  | 13 => (4, 10)
  47  | 14 => (6, 7)
  48  | 15 => (6, 9)
  49  | 16 => (6, 10)
  50  | 17 => (7, 10)
  51  | 18 => (9, 10)
  52  | 19 => (1, 2)
  53  | 20 => (1, 5)
  54  | 21 => (1, 8)
  55  | 22 => (1, 11)
  56  | 23 => (2, 5)
  57  | 24 => (2, 8)
  58  | 25 => (2, 11)
  59  | 26 => (4, 5)
  60  | 27 => (4, 11)
  61  | 28 => (5, 11)
  62  | 29 => (7, 8)
  63  | 30 => (7, 11)
  64  | 31 => (8, 11)
  65  | 32 => (10, 11)
  66  | ⟨n+33, h⟩ => absurd h (by omega)
  67
  68def globalSqEdge : E → ℝ
  69  | 0 => 1
  70  | 1 => 1
  71  | 2 => 1
  72  | 3 => 2
  73  | 4 => 2
  74  | 5 => 2
  75  | 6 => 3
  76  | 7 => 1
  77  | 8 => 1
  78  | 9 => 2
  79  | 10 => 1
  80  | 11 => 1
  81  | 12 => 2
  82  | 13 => 1
  83  | 14 => 1
  84  | 15 => 1
  85  | 16 => 2
  86  | 17 => 1
  87  | 18 => 1
  88  | 19 => 1
  89  | 20 => 2
  90  | 21 => 2
  91  | 22 => 3
  92  | 23 => 1
  93  | 24 => 1
  94  | 25 => 2
  95  | 26 => 1
  96  | 27 => 2
  97  | 28 => 1
  98  | 29 => 1
  99  | 30 => 2
 100  | 31 => 1
 101  | 32 => 1
 102  | ⟨n+33, h⟩ => absurd h (by omega)
 103
 104/-- Twelve tetrahedra: six in the left cube and six in the right cube. -/
 105def tetVerts : T → Fin 4 → V
 106  | 0, 0 => 0
 107  | 0, 1 => 1
 108  | 0, 2 => 4
 109  | 0, 3 => 10
 110  | 1, 0 => 0
 111  | 1, 1 => 1
 112  | 1, 2 => 7
 113  | 1, 3 => 10
 114  | 2, 0 => 0
 115  | 2, 1 => 3
 116  | 2, 2 => 4
 117  | 2, 3 => 10
 118  | 3, 0 => 0
 119  | 3, 1 => 3
 120  | 3, 2 => 9
 121  | 3, 3 => 10
 122  | 4, 0 => 0
 123  | 4, 1 => 6
 124  | 4, 2 => 7
 125  | 4, 3 => 10
 126  | 5, 0 => 0
 127  | 5, 1 => 6
 128  | 5, 2 => 9
 129  | 5, 3 => 10
 130  | 6, 0 => 1
 131  | 6, 1 => 2
 132  | 6, 2 => 5
 133  | 6, 3 => 11
 134  | 7, 0 => 1
 135  | 7, 1 => 2
 136  | 7, 2 => 8
 137  | 7, 3 => 11
 138  | 8, 0 => 1
 139  | 8, 1 => 4
 140  | 8, 2 => 5
 141  | 8, 3 => 11
 142  | 9, 0 => 1
 143  | 9, 1 => 4
 144  | 9, 2 => 10
 145  | 9, 3 => 11
 146  | 10, 0 => 1
 147  | 10, 1 => 7
 148  | 10, 2 => 8
 149  | 10, 3 => 11
 150  | 11, 0 => 1
 151  | 11, 1 => 7
 152  | 11, 2 => 10
 153  | 11, 3 => 11
 154
 155/-- Global edge representative for every local tetrahedral edge slot. -/
 156def localEdgeOf : T → Fin 6 → E
 157  | 0, 0 => 0
 158  | 0, 1 => 3
 159  | 0, 2 => 6
 160  | 0, 3 => 7
 161  | 0, 4 => 9
 162  | 0, 5 => 13
 163  | 1, 0 => 0
 164  | 1, 1 => 4
 165  | 1, 2 => 6
 166  | 1, 3 => 8
 167  | 1, 4 => 9
 168  | 1, 5 => 17
 169  | 2, 0 => 1
 170  | 2, 1 => 3
 171  | 2, 2 => 6
 172  | 2, 3 => 10
 173  | 2, 4 => 12
 174  | 2, 5 => 13
 175  | 3, 0 => 1
 176  | 3, 1 => 5
 177  | 3, 2 => 6
 178  | 3, 3 => 11
 179  | 3, 4 => 12
 180  | 3, 5 => 18
 181  | 4, 0 => 2
 182  | 4, 1 => 4
 183  | 4, 2 => 6
 184  | 4, 3 => 14
 185  | 4, 4 => 16
 186  | 4, 5 => 17
 187  | 5, 0 => 2
 188  | 5, 1 => 5
 189  | 5, 2 => 6
 190  | 5, 3 => 15
 191  | 5, 4 => 16
 192  | 5, 5 => 18
 193  | 6, 0 => 19
 194  | 6, 1 => 20
 195  | 6, 2 => 22
 196  | 6, 3 => 23
 197  | 6, 4 => 25
 198  | 6, 5 => 28
 199  | 7, 0 => 19
 200  | 7, 1 => 21
 201  | 7, 2 => 22
 202  | 7, 3 => 24
 203  | 7, 4 => 25
 204  | 7, 5 => 31
 205  | 8, 0 => 7
 206  | 8, 1 => 20
 207  | 8, 2 => 22
 208  | 8, 3 => 26
 209  | 8, 4 => 27
 210  | 8, 5 => 28
 211  | 9, 0 => 7
 212  | 9, 1 => 9
 213  | 9, 2 => 22
 214  | 9, 3 => 13
 215  | 9, 4 => 27
 216  | 9, 5 => 32
 217  | 10, 0 => 8
 218  | 10, 1 => 21
 219  | 10, 2 => 22
 220  | 10, 3 => 29
 221  | 10, 4 => 30
 222  | 10, 5 => 31
 223  | 11, 0 => 8
 224  | 11, 1 => 9
 225  | 11, 2 => 22
 226  | 11, 3 => 17
 227  | 11, 4 => 30
 228  | 11, 5 => 32
 229
 230def edgeInTet (e : E) (τ : T) : Option (Fin 6) :=
 231  if e = localEdgeOf τ 0 then some 0 else
 232  if e = localEdgeOf τ 1 then some 1 else
 233  if e = localEdgeOf τ 2 then some 2 else
 234  if e = localEdgeOf τ 3 then some 3 else
 235  if e = localEdgeOf τ 4 then some 4 else
 236  if e = localEdgeOf τ 5 then some 5 else
 237  none
 238
 239def twoCubeStrip : Triangulation3D where
 240  nV := 12
 241  nE := 33
 242  nT := 12
 243  edgeVerts := edgeVerts
 244  tetVerts := tetVerts
 245  edgeInTet := edgeInTet
 246  tet := fun _ => FreudenthalCubeTriangulation.freudenthalTet
 247
 248theorem edgeInTet_iff_localEdgeOf (e : E) (τ : T) (f : Fin 6) :
 249    edgeInTet e τ = some f ↔ e = localEdgeOf τ f := by
 250  native_decide +revert
 251
 252theorem local_sqEdge_eq_global
 253    (e : E) (τ : T) (f : Fin 6) (h : edgeInTet e τ = some f) :
 254    FreudenthalCubeTriangulation.freudenthalTet.sqEdge f = globalSqEdge e := by
 255  have he : e = localEdgeOf τ f := (edgeInTet_iff_localEdgeOf e τ f).1 h
 256  subst e
 257  fin_cases τ <;> fin_cases f <;>
 258    simp [localEdgeOf, FreudenthalCubeTriangulation.freudenthalTet,
 259      FreudenthalCubeTriangulation.freudenthalTetSqEdges, globalSqEdge]
 260
 261theorem edgeInTet_vertices
 262    (e : E) (τ : T) (f : Fin 6) (h : edgeInTet e τ = some f) :
 263      let ev := edgeVerts e
 264      let tv := ReggeRigorousFoundation.edgeVertices f
 265      (tetVerts τ tv.1 = ev.1 ∧ tetVerts τ tv.2 = ev.2) ∨
 266        (tetVerts τ tv.1 = ev.2 ∧ tetVerts τ tv.2 = ev.1) := by
 267  have he : e = localEdgeOf τ f := (edgeInTet_iff_localEdgeOf e τ f).1 h
 268  subst e
 269  fin_cases τ <;> fin_cases f <;>
 270    simp [localEdgeOf, edgeVerts, tetVerts,
 271      ReggeRigorousFoundation.edgeVertices] at h ⊢
 272
 273theorem localEdge_complete (τ : T) (f : Fin 6) :
 274    ∃ e : E, edgeInTet e τ = some f := by
 275  exact ⟨localEdgeOf τ f, (edgeInTet_iff_localEdgeOf (localEdgeOf τ f) τ f).2 rfl⟩
 276
 277def twoCubeStrip_incidenceConsistent :
 278    IncidenceConsistent twoCubeStrip where
 279  globalSqEdge := globalSqEdge
 280  edgeInTet_vertices := by
 281    intro e τ f h
 282    exact edgeInTet_vertices e τ f h
 283  local_sqEdge_eq_global := by
 284    intro e τ f h
 285    exact local_sqEdge_eq_global e τ f h
 286  localEdge_complete := by
 287    intro τ f
 288    exact localEdge_complete τ f
 289  local_schlaefli := by
 290    intro τ
 291    exact schlaefliTetrahedronClosedForm FreudenthalCubeTriangulation.freudenthalTet
 292
 293def twoCubeStrip_edgeSlotPartition :
 294    IncidenceEdgeSlotPartition twoCubeStrip twoCubeStrip_incidenceConsistent where
 295  localEdgeOf := localEdgeOf
 296  edgeInTet_iff := by
 297    intro e τ f
 298    exact edgeInTet_iff_localEdgeOf e τ f
 299
 300def twoCubeStrip_edgeSlotBookkeeping :
 301    IncidenceEdgeSlotBookkeeping twoCubeStrip twoCubeStrip_incidenceConsistent :=
 302  incidenceEdgeSlotBookkeeping_of_partition
 303    twoCubeStrip twoCubeStrip_incidenceConsistent twoCubeStrip_edgeSlotPartition
 304
 305end
 306
 307end FreudenthalTwoCubeStrip
 308end Geometry
 309end IndisputableMonolith
 310