IndisputableMonolith.Geometry.PeriodicFreudenthalTorus
IndisputableMonolith/Geometry/PeriodicFreudenthalTorus.lean · 729 lines · 59 declarations
show as:
view math explainer →
1import IndisputableMonolith.Geometry.FreudenthalCubeTriangulation
2
3/-!
4# Periodic Freudenthal Torus Model
5
6This module gives the scalable target shape for an arbitrary periodic
7Freudenthal tiling. It does not enumerate a concrete `n × m × k` finite
8mesh yet; instead it defines the typed periodic vertex/edge/tetrahedron
9model and proves that any finite `Triangulation3D` encoding this model has
10the global `IncidenceEdgeSlotPartition` needed by the nonlinear Regge
11first-variation theorem.
12
13The point is to isolate the remaining work: a finite encoder from the typed
14periodic torus into `Fin nV`, `Fin nE`, `Fin nT`.
15-/
16
17namespace IndisputableMonolith
18namespace Geometry
19namespace PeriodicFreudenthalTorus
20
21open ReggeTriangulation3D
22open Triangulation3DConsistency
23open ReggeActionFirstVariation
24
25noncomputable section
26
27/-- Periodic cubic vertices. -/
28abbrev Vertex (Nx Ny Nz : ℕ) := Fin Nx × Fin Ny × Fin Nz
29
30def bit : Bool → ℕ
31 | false => 0
32 | true => 1
33
34def addBit {N : ℕ} [NeZero N] (i : Fin N) (b : Bool) : Fin N :=
35 ⟨(i.val + bit b) % N, Nat.mod_lt _ (Nat.pos_of_neZero N)⟩
36
37@[simp] theorem addBit_false {N : ℕ} [NeZero N] (i : Fin N) :
38 addBit i false = i := by
39 ext
40 simp [addBit, bit, Nat.mod_eq_of_lt i.isLt]
41
42@[simp] theorem addBit_true_eq_mk {N : ℕ} [NeZero N] (i : Fin N) :
43 addBit i true =
44 ⟨(i.val + 1) % N, Nat.mod_lt _ (Nat.pos_of_neZero N)⟩ := by
45 rfl
46
47@[simp] theorem addBit_false_after_true {N : ℕ} [NeZero N] (i : Fin N) :
48 addBit (addBit i true) false = addBit i true := by
49 simp
50
51@[simp] theorem addBit_true_after_false {N : ℕ} [NeZero N] (i : Fin N) :
52 addBit (addBit i false) true = addBit i true := by
53 simp
54
55theorem addBit_true_ne_self {N : ℕ} [NeZero N] (hN : 2 < N) (i : Fin N) :
56 addBit i true ≠ i := by
57 intro h
58 have hval : (i.val + 1) % N = i.val := by
59 simpa [addBit, bit] using congrArg Fin.val h
60 have hcases : i.val + 1 < N ∨ i.val + 1 = N := by
61 omega
62 cases hcases with
63 | inl hlt =>
64 have hmod : (i.val + 1) % N = i.val + 1 := Nat.mod_eq_of_lt hlt
65 omega
66 | inr heq =>
67 have hmod : (i.val + 1) % N = 0 := by
68 rw [heq, Nat.mod_self]
69 omega
70
71def addBits {Nx Ny Nz : ℕ} [NeZero Nx] [NeZero Ny] [NeZero Nz]
72 (v : Vertex Nx Ny Nz) (dx dy dz : Bool) : Vertex Nx Ny Nz :=
73 (addBit v.1 dx, addBit v.2.1 dy, addBit v.2.2 dz)
74
75/-- Nonzero positive cube displacements. -/
76def dispBits : Fin 7 → Bool × Bool × Bool
77 | 0 => (true, false, false)
78 | 1 => (false, true, false)
79 | 2 => (false, false, true)
80 | 3 => (true, true, false)
81 | 4 => (true, false, true)
82 | 5 => (false, true, true)
83 | 6 => (true, true, true)
84
85/-- Local cube vertex offsets, using binary cube labels. -/
86def vertexBits : Fin 8 → Bool × Bool × Bool
87 | 0 => (false, false, false)
88 | 1 => (true, false, false)
89 | 2 => (false, true, false)
90 | 3 => (true, true, false)
91 | 4 => (false, false, true)
92 | 5 => (true, false, true)
93 | 6 => (false, true, true)
94 | 7 => (true, true, true)
95
96def addVertexBits {Nx Ny Nz : ℕ} [NeZero Nx] [NeZero Ny] [NeZero Nz]
97 (v : Vertex Nx Ny Nz) (a : Fin 8) : Vertex Nx Ny Nz :=
98 let b := vertexBits a
99 addBits v b.1 b.2.1 b.2.2
100
101theorem addBit_true_injective {N : ℕ} [NeZero N] :
102 Function.Injective (fun i : Fin N => addBit i true) := by
103 intro i j h
104 ext
105 have hval : (i.val + 1) % N = (j.val + 1) % N := by
106 simpa [addBit, bit] using congrArg Fin.val h
107 have hi : i.val + 1 < N ∨ i.val + 1 = N := by
108 omega
109 have hj : j.val + 1 < N ∨ j.val + 1 = N := by
110 omega
111 cases hi with
112 | inl hi_lt =>
113 have himod : (i.val + 1) % N = i.val + 1 := Nat.mod_eq_of_lt hi_lt
114 cases hj with
115 | inl hj_lt =>
116 have hjmod : (j.val + 1) % N = j.val + 1 := Nat.mod_eq_of_lt hj_lt
117 omega
118 | inr hj_eq =>
119 have hjmod : (j.val + 1) % N = 0 := by
120 rw [hj_eq, Nat.mod_self]
121 omega
122 | inr hi_eq =>
123 have himod : (i.val + 1) % N = 0 := by
124 rw [hi_eq, Nat.mod_self]
125 cases hj with
126 | inl hj_lt =>
127 have hjmod : (j.val + 1) % N = j.val + 1 := Nat.mod_eq_of_lt hj_lt
128 omega
129 | inr hj_eq =>
130 omega
131
132theorem addBit_injective {N : ℕ} [NeZero N] (b : Bool) :
133 Function.Injective (fun i : Fin N => addBit i b) := by
134 cases b
135 · intro i j h
136 simpa using h
137 · exact addBit_true_injective
138
139theorem addBits_injective
140 {Nx Ny Nz : ℕ} [NeZero Nx] [NeZero Ny] [NeZero Nz]
141 (dx dy dz : Bool) :
142 Function.Injective (fun v : Vertex Nx Ny Nz => addBits v dx dy dz) := by
143 intro v w h
144 rcases v with ⟨vx, vy, vz⟩
145 rcases w with ⟨wx, wy, wz⟩
146 simp [addBits] at h ⊢
147 exact ⟨addBit_injective dx h.1, addBit_injective dy h.2.1,
148 addBit_injective dz h.2.2⟩
149
150theorem addVertexBits_injective
151 {Nx Ny Nz : ℕ} [NeZero Nx] [NeZero Ny] [NeZero Nz]
152 (a : Fin 8) :
153 Function.Injective (fun v : Vertex Nx Ny Nz => addVertexBits v a) := by
154 intro v w h
155 unfold addVertexBits at h
156 exact addBits_injective _ _ _ h
157
158theorem addVertexBits_surjective
159 {Nx Ny Nz : ℕ} [NeZero Nx] [NeZero Ny] [NeZero Nz]
160 (a : Fin 8) :
161 Function.Surjective (fun v : Vertex Nx Ny Nz => addVertexBits v a) :=
162 Finite.surjective_of_injective (addVertexBits_injective a)
163
164theorem existsUnique_addVertexBits_eq
165 {Nx Ny Nz : ℕ} [NeZero Nx] [NeZero Ny] [NeZero Nz]
166 (a : Fin 8) (target : Vertex Nx Ny Nz) :
167 ∃! cell : Vertex Nx Ny Nz, target = addVertexBits cell a := by
168 rcases addVertexBits_surjective a target with ⟨cell, hcell⟩
169 refine ⟨cell, hcell.symm, ?_⟩
170 intro other hother
171 exact addVertexBits_injective a (hother.symm.trans hcell.symm)
172
173/-- Summing a constant over the unique periodic cell solving a translated
174base-vertex equation returns that constant. -/
175theorem sum_ite_eq_of_addVertexBits
176 {Nx Ny Nz : ℕ} [NeZero Nx] [NeZero Ny] [NeZero Nz]
177 (a : Fin 8) (target : Vertex Nx Ny Nz) (c : ℝ) :
178 (∑ cell : Vertex Nx Ny Nz,
179 if target = addVertexBits cell a then c else 0) = c := by
180 classical
181 rcases addVertexBits_surjective a target with ⟨cell0, hcell0⟩
182 rw [Finset.sum_eq_single cell0]
183 · simp [hcell0]
184 · intro cell _ hne
185 have hneq : target ≠ addVertexBits cell a := by
186 intro h
187 apply hne
188 exact addVertexBits_injective a (h.symm.trans hcell0.symm)
189 simp [hneq]
190 · intro hnot
191 exact (hnot (Finset.mem_univ cell0)).elim
192
193/-- A positive-displacement periodic edge, represented by its lower/base
194vertex and one of the seven positive cube displacements. -/
195structure PeriodicEdge (Nx Ny Nz : ℕ) [NeZero Nx] [NeZero Ny] [NeZero Nz] where
196 base : Vertex Nx Ny Nz
197 disp : Fin 7
198deriving DecidableEq, Fintype
199
200/-- Endpoints of a positive-displacement periodic edge. -/
201def PeriodicEdge.endpoints {Nx Ny Nz : ℕ} [NeZero Nx] [NeZero Ny] [NeZero Nz]
202 (e : PeriodicEdge Nx Ny Nz) : Vertex Nx Ny Nz × Vertex Nx Ny Nz :=
203 let d := dispBits e.disp
204 (e.base, addBits e.base d.1 d.2.1 d.2.2)
205
206theorem PeriodicEdge.endpoints_ne
207 {Nx Ny Nz : ℕ} [NeZero Nx] [NeZero Ny] [NeZero Nz]
208 (hx : 2 < Nx) (hy : 2 < Ny) (hz : 2 < Nz)
209 (e : PeriodicEdge Nx Ny Nz) :
210 e.endpoints.1 ≠ e.endpoints.2 := by
211 cases e with
212 | mk base disp =>
213 fin_cases disp
214 · intro h
215 simp [PeriodicEdge.endpoints, dispBits, addBits] at h
216 exact addBit_true_ne_self hx base.1 ((congrArg Prod.fst h).symm)
217 · intro h
218 simp [PeriodicEdge.endpoints, dispBits, addBits] at h
219 exact addBit_true_ne_self hy base.2.1
220 ((congrArg (fun v : Vertex Nx Ny Nz => v.2.1) h).symm)
221 · intro h
222 simp [PeriodicEdge.endpoints, dispBits, addBits] at h
223 exact addBit_true_ne_self hz base.2.2
224 ((congrArg (fun v : Vertex Nx Ny Nz => v.2.2) h).symm)
225 · intro h
226 simp [PeriodicEdge.endpoints, dispBits, addBits] at h
227 exact addBit_true_ne_self hx base.1 ((congrArg Prod.fst h).symm)
228 · intro h
229 simp [PeriodicEdge.endpoints, dispBits, addBits] at h
230 exact addBit_true_ne_self hx base.1 ((congrArg Prod.fst h).symm)
231 · intro h
232 simp [PeriodicEdge.endpoints, dispBits, addBits] at h
233 exact addBit_true_ne_self hy base.2.1
234 ((congrArg (fun v : Vertex Nx Ny Nz => v.2.1) h).symm)
235 · intro h
236 simp [PeriodicEdge.endpoints, dispBits, addBits] at h
237 exact addBit_true_ne_self hx base.1 ((congrArg Prod.fst h).symm)
238
239/-- Base local cube vertex for each of the 19 one-cube Freudenthal edge
240representatives. -/
241def cubeEdgeBase : Fin 19 → Fin 8
242 | 0 => 0
243 | 1 => 0
244 | 2 => 0
245 | 3 => 0
246 | 4 => 0
247 | 5 => 0
248 | 6 => 0
249 | 7 => 1
250 | 8 => 1
251 | 9 => 1
252 | 10 => 2
253 | 11 => 2
254 | 12 => 2
255 | 13 => 3
256 | 14 => 4
257 | 15 => 4
258 | 16 => 4
259 | 17 => 5
260 | 18 => 6
261 | ⟨n+19, h⟩ => absurd h (by omega)
262
263/-- Positive displacement for each one-cube Freudenthal edge representative. -/
264def cubeEdgeDisp : Fin 19 → Fin 7
265 | 0 => 0 -- x
266 | 1 => 1 -- y
267 | 2 => 2 -- z
268 | 3 => 3 -- x+y
269 | 4 => 4 -- x+z
270 | 5 => 5 -- y+z
271 | 6 => 6 -- x+y+z
272 | 7 => 1
273 | 8 => 2
274 | 9 => 5
275 | 10 => 0
276 | 11 => 2
277 | 12 => 4
278 | 13 => 2
279 | 14 => 0
280 | 15 => 1
281 | 16 => 3
282 | 17 => 1
283 | 18 => 0
284 | ⟨n+19, h⟩ => absurd h (by omega)
285
286/-- The translated global edge of a local Freudenthal tetrahedral edge slot. -/
287def localEdgeOf {Nx Ny Nz : ℕ} [NeZero Nx] [NeZero Ny] [NeZero Nz]
288 (cell : Vertex Nx Ny Nz) (tet : Fin 6) (f : Fin 6) :
289 PeriodicEdge Nx Ny Nz :=
290 let e := FreudenthalCubeTriangulation.localEdgeOf tet f
291 { base := addVertexBits cell (cubeEdgeBase e), disp := cubeEdgeDisp e }
292
293/-- Periodic Freudenthal tetrahedra: one of the six Freudenthal tetrahedra
294inside each periodic cubic cell. -/
295abbrev PeriodicTet (Nx Ny Nz : ℕ) := Vertex Nx Ny Nz × Fin 6
296
297/-- Canonical finite index set for periodic vertices. This is the first
298concrete encoder ingredient: every periodic vertex is now indexed by a `Fin`
299type of the right cardinality. -/
300noncomputable def vertexFinEquiv
301 (Nx Ny Nz : ℕ) [NeZero Nx] [NeZero Ny] [NeZero Nz] :
302 Fin (Fintype.card (Vertex Nx Ny Nz)) ≃ Vertex Nx Ny Nz :=
303 (Fintype.equivFin (Vertex Nx Ny Nz)).symm
304
305/-- Canonical finite index set for positive-displacement periodic edges. -/
306noncomputable def edgeFinEquiv
307 (Nx Ny Nz : ℕ) [NeZero Nx] [NeZero Ny] [NeZero Nz] :
308 Fin (Fintype.card (PeriodicEdge Nx Ny Nz)) ≃ PeriodicEdge Nx Ny Nz :=
309 (Fintype.equivFin (PeriodicEdge Nx Ny Nz)).symm
310
311/-- Canonical finite index set for periodic Freudenthal tetrahedra. -/
312noncomputable def tetFinEquiv
313 (Nx Ny Nz : ℕ) [NeZero Nx] [NeZero Ny] [NeZero Nz] :
314 Fin (Fintype.card (PeriodicTet Nx Ny Nz)) ≃ PeriodicTet Nx Ny Nz :=
315 (Fintype.equivFin (PeriodicTet Nx Ny Nz)).symm
316
317/-- Computable local edge-slot lookup for the canonical periodic skeleton. -/
318def canonicalEdgeSlot?
319 {Nx Ny Nz : ℕ} [NeZero Nx] [NeZero Ny] [NeZero Nz]
320 (e : PeriodicEdge Nx Ny Nz) (cell : Vertex Nx Ny Nz) (tet : Fin 6) :
321 Option (Fin 6) :=
322 if e = localEdgeOf cell tet 0 then some 0
323 else if e = localEdgeOf cell tet 1 then some 1
324 else if e = localEdgeOf cell tet 2 then some 2
325 else if e = localEdgeOf cell tet 3 then some 3
326 else if e = localEdgeOf cell tet 4 then some 4
327 else if e = localEdgeOf cell tet 5 then some 5
328 else none
329
330theorem canonicalEdgeSlot_eq_some_implies
331 {Nx Ny Nz : ℕ} [NeZero Nx] [NeZero Ny] [NeZero Nz]
332 {e : PeriodicEdge Nx Ny Nz} {cell : Vertex Nx Ny Nz}
333 {tet : Fin 6} {f : Fin 6}
334 (h : canonicalEdgeSlot? e cell tet = some f) :
335 e = localEdgeOf cell tet f := by
336 unfold canonicalEdgeSlot? at h
337 split_ifs at h with h0 h1 h2 h3 h4 h5
338 · cases h
339 exact h0
340 · cases h
341 exact h1
342 · cases h
343 exact h2
344 · cases h
345 exact h3
346 · cases h
347 exact h4
348 · cases h
349 exact h5
350
351/-- Reverse edge-slot implication, reduced to the local no-duplication theorem.
352The remaining arithmetic content is proving `CanonicalPeriodicLocalEdgeNoDup`
353from the side-length assumptions `Nx,Ny,Nz > 2`. -/
354theorem canonicalEdgeSlot_eq_some_of_noDup
355 {Nx Ny Nz : ℕ} [NeZero Nx] [NeZero Ny] [NeZero Nz]
356 {e : PeriodicEdge Nx Ny Nz} {cell : Vertex Nx Ny Nz}
357 {tet : Fin 6} {f : Fin 6}
358 (hNoDup :
359 ∀ f g : Fin 6, localEdgeOf cell tet f = localEdgeOf cell tet g → f = g)
360 (h : e = localEdgeOf cell tet f) :
361 canonicalEdgeSlot? e cell tet = some f := by
362 subst e
363 unfold canonicalEdgeSlot?
364 split_ifs with h0 h1 h2 h3 h4 h5
365 · have hf : f = 0 := hNoDup f 0 h0
366 subst f
367 rfl
368 · have hf : f = 1 := hNoDup f 1 h1
369 subst f
370 rfl
371 · have hf : f = 2 := hNoDup f 2 h2
372 subst f
373 rfl
374 · have hf : f = 3 := hNoDup f 3 h3
375 subst f
376 rfl
377 · have hf : f = 4 := hNoDup f 4 h4
378 subst f
379 rfl
380 · have hf : f = 5 := hNoDup f 5 h5
381 subst f
382 rfl
383 · fin_cases f <;> simp at h0 h1 h2 h3 h4 h5
384
385/-- Canonical endpoint map for positive-displacement periodic edges, expressed
386in the finite vertex index set. -/
387def canonicalEdgeVerts
388 (Nx Ny Nz : ℕ) [NeZero Nx] [NeZero Ny] [NeZero Nz]
389 (e : Fin (Fintype.card (PeriodicEdge Nx Ny Nz))) :
390 Fin (Fintype.card (Vertex Nx Ny Nz)) ×
391 Fin (Fintype.card (Vertex Nx Ny Nz)) :=
392 let edge := edgeFinEquiv Nx Ny Nz e
393 let endpoints := edge.endpoints
394 ((vertexFinEquiv Nx Ny Nz).symm endpoints.1,
395 (vertexFinEquiv Nx Ny Nz).symm endpoints.2)
396
397/-- Canonical tetrahedron vertex map for the six-tetrahedron Freudenthal
398decomposition in every periodic cube. -/
399def canonicalTetVerts
400 (Nx Ny Nz : ℕ) [NeZero Nx] [NeZero Ny] [NeZero Nz]
401 (τ : Fin (Fintype.card (PeriodicTet Nx Ny Nz))) (k : Fin 4) :
402 Fin (Fintype.card (Vertex Nx Ny Nz)) :=
403 let cellTet := tetFinEquiv Nx Ny Nz τ
404 let localVertex := FreudenthalCubeTriangulation.tetVerts cellTet.2 k
405 (vertexFinEquiv Nx Ny Nz).symm (addVertexBits cellTet.1 localVertex)
406
407/-- Canonical edge-in-tetrahedron lookup for the finite periodic skeleton. -/
408def canonicalEdgeInTet
409 (Nx Ny Nz : ℕ) [NeZero Nx] [NeZero Ny] [NeZero Nz]
410 (e : Fin (Fintype.card (PeriodicEdge Nx Ny Nz)))
411 (τ : Fin (Fintype.card (PeriodicTet Nx Ny Nz))) : Option (Fin 6) :=
412 let cellTet := tetFinEquiv Nx Ny Nz τ
413 canonicalEdgeSlot? (edgeFinEquiv Nx Ny Nz e) cellTet.1 cellTet.2
414
415theorem canonicalEdgeInTet_eq_some_implies
416 (Nx Ny Nz : ℕ) [NeZero Nx] [NeZero Ny] [NeZero Nz]
417 (e : Fin (Fintype.card (PeriodicEdge Nx Ny Nz)))
418 (τ : Fin (Fintype.card (PeriodicTet Nx Ny Nz))) {f : Fin 6}
419 (h : canonicalEdgeInTet Nx Ny Nz e τ = some f) :
420 edgeFinEquiv Nx Ny Nz e =
421 localEdgeOf (tetFinEquiv Nx Ny Nz τ).1 (tetFinEquiv Nx Ny Nz τ).2 f := by
422 unfold canonicalEdgeInTet at h
423 exact canonicalEdgeSlot_eq_some_implies h
424
425/-- Remaining wraparound/no-duplication target for turning the canonical
426periodic skeleton into a full `EncodedPeriodicFreudenthalTorus`. -/
427def CanonicalPeriodicLocalEdgeNoDup
428 (Nx Ny Nz : ℕ) [NeZero Nx] [NeZero Ny] [NeZero Nz] : Prop :=
429 ∀ (cell : Vertex Nx Ny Nz) (tet : Fin 6) (f g : Fin 6),
430 localEdgeOf cell tet f = localEdgeOf cell tet g → f = g
431
432theorem canonicalPeriodicLocalEdgeNoDup
433 (Nx Ny Nz : ℕ) [NeZero Nx] [NeZero Ny] [NeZero Nz] :
434 CanonicalPeriodicLocalEdgeNoDup Nx Ny Nz := by
435 intro cell tet f g h
436 fin_cases tet <;> fin_cases f <;> fin_cases g <;>
437 simp [localEdgeOf, FreudenthalCubeTriangulation.localEdgeOf,
438 cubeEdgeDisp] at h ⊢
439
440theorem canonicalEdgeInTet_iff_of_noDup
441 (Nx Ny Nz : ℕ) [NeZero Nx] [NeZero Ny] [NeZero Nz]
442 (hNoDup : CanonicalPeriodicLocalEdgeNoDup Nx Ny Nz)
443 (e : Fin (Fintype.card (PeriodicEdge Nx Ny Nz)))
444 (τ : Fin (Fintype.card (PeriodicTet Nx Ny Nz))) (f : Fin 6) :
445 canonicalEdgeInTet Nx Ny Nz e τ = some f ↔
446 edgeFinEquiv Nx Ny Nz e =
447 localEdgeOf (tetFinEquiv Nx Ny Nz τ).1 (tetFinEquiv Nx Ny Nz τ).2 f := by
448 constructor
449 · intro h
450 exact canonicalEdgeInTet_eq_some_implies Nx Ny Nz e τ h
451 · intro h
452 unfold canonicalEdgeInTet
453 exact canonicalEdgeSlot_eq_some_of_noDup
454 (fun f g hg => hNoDup (tetFinEquiv Nx Ny Nz τ).1
455 (tetFinEquiv Nx Ny Nz τ).2 f g hg)
456 h
457
458/-- Squared edge length determined only by the positive displacement class. -/
459def periodicDispSqEdge : Fin 7 → ℝ
460 | 0 => 1
461 | 1 => 1
462 | 2 => 1
463 | 3 => 2
464 | 4 => 2
465 | 5 => 2
466 | 6 => 3
467
468def canonicalGlobalSqEdge
469 (Nx Ny Nz : ℕ) [NeZero Nx] [NeZero Ny] [NeZero Nz]
470 (e : Fin (Fintype.card (PeriodicEdge Nx Ny Nz))) : ℝ :=
471 periodicDispSqEdge ((edgeFinEquiv Nx Ny Nz e).disp)
472
473theorem freudenthalTet_sqEdge_eq_periodicDispSqEdge_localEdgeOf
474 {Nx Ny Nz : ℕ} [NeZero Nx] [NeZero Ny] [NeZero Nz]
475 (cell : Vertex Nx Ny Nz) (tet f : Fin 6) :
476 FreudenthalCubeTriangulation.freudenthalTet.sqEdge f =
477 periodicDispSqEdge ((localEdgeOf cell tet f).disp) := by
478 fin_cases tet <;> fin_cases f <;>
479 simp [localEdgeOf, FreudenthalCubeTriangulation.localEdgeOf,
480 FreudenthalCubeTriangulation.freudenthalTet,
481 FreudenthalCubeTriangulation.freudenthalTetSqEdges,
482 cubeEdgeDisp, periodicDispSqEdge]
483
484theorem canonicalLocalSqEdge_eq_global
485 (Nx Ny Nz : ℕ) [NeZero Nx] [NeZero Ny] [NeZero Nz]
486 (e : Fin (Fintype.card (PeriodicEdge Nx Ny Nz)))
487 (τ : Fin (Fintype.card (PeriodicTet Nx Ny Nz))) (f : Fin 6)
488 (h : canonicalEdgeInTet Nx Ny Nz e τ = some f) :
489 FreudenthalCubeTriangulation.freudenthalTet.sqEdge f =
490 canonicalGlobalSqEdge Nx Ny Nz e := by
491 have he := canonicalEdgeInTet_eq_some_implies Nx Ny Nz e τ h
492 unfold canonicalGlobalSqEdge
493 rw [he]
494 exact freudenthalTet_sqEdge_eq_periodicDispSqEdge_localEdgeOf
495 (tetFinEquiv Nx Ny Nz τ).1 (tetFinEquiv Nx Ny Nz τ).2 f
496
497theorem canonicalLocalEdge_complete
498 (Nx Ny Nz : ℕ) [NeZero Nx] [NeZero Ny] [NeZero Nz]
499 (hNoDup : CanonicalPeriodicLocalEdgeNoDup Nx Ny Nz)
500 (τ : Fin (Fintype.card (PeriodicTet Nx Ny Nz))) (f : Fin 6) :
501 ∃ e : Fin (Fintype.card (PeriodicEdge Nx Ny Nz)),
502 canonicalEdgeInTet Nx Ny Nz e τ = some f := by
503 let edge := localEdgeOf (tetFinEquiv Nx Ny Nz τ).1 (tetFinEquiv Nx Ny Nz τ).2 f
504 refine ⟨(edgeFinEquiv Nx Ny Nz).symm edge, ?_⟩
505 have hEdge :
506 edgeFinEquiv Nx Ny Nz ((edgeFinEquiv Nx Ny Nz).symm edge) =
507 localEdgeOf (tetFinEquiv Nx Ny Nz τ).1 (tetFinEquiv Nx Ny Nz τ).2 f := by
508 simp [edge]
509 exact (canonicalEdgeInTet_iff_of_noDup Nx Ny Nz hNoDup
510 ((edgeFinEquiv Nx Ny Nz).symm edge) τ f).2 hEdge
511
512/-- The concrete finite periodic Freudenthal triangulation skeleton. This is
513not yet the full encoded torus certificate because incidence consistency still
514requires the wraparound no-duplication and local/global squared-edge proofs. -/
515def canonicalPeriodicTriangulation
516 (Nx Ny Nz : ℕ) [NeZero Nx] [NeZero Ny] [NeZero Nz] :
517 Triangulation3D where
518 nV := Fintype.card (Vertex Nx Ny Nz)
519 nE := Fintype.card (PeriodicEdge Nx Ny Nz)
520 nT := Fintype.card (PeriodicTet Nx Ny Nz)
521 edgeVerts := canonicalEdgeVerts Nx Ny Nz
522 tetVerts := canonicalTetVerts Nx Ny Nz
523 edgeInTet := canonicalEdgeInTet Nx Ny Nz
524 tet := fun _ => FreudenthalCubeTriangulation.freudenthalTet
525
526def canonicalPeriodicEdgeEquiv
527 (Nx Ny Nz : ℕ) [NeZero Nx] [NeZero Ny] [NeZero Nz] :
528 Fin (canonicalPeriodicTriangulation Nx Ny Nz).nE ≃
529 PeriodicEdge Nx Ny Nz :=
530 edgeFinEquiv Nx Ny Nz
531
532def canonicalPeriodicTetEquiv
533 (Nx Ny Nz : ℕ) [NeZero Nx] [NeZero Ny] [NeZero Nz] :
534 Fin (canonicalPeriodicTriangulation Nx Ny Nz).nT ≃
535 PeriodicTet Nx Ny Nz :=
536 tetFinEquiv Nx Ny Nz
537
538/-- Remaining endpoint-orientation condition for the canonical periodic
539skeleton. This is the modular-arithmetic part of incidence consistency:
540local Freudenthal edge endpoints must match the global periodic edge endpoints
541up to orientation. -/
542def CanonicalPeriodicEndpointIncidence
543 (Nx Ny Nz : ℕ) [NeZero Nx] [NeZero Ny] [NeZero Nz] : Prop :=
544 ∀ e τ f, canonicalEdgeInTet Nx Ny Nz e τ = some f →
545 let ev := canonicalEdgeVerts Nx Ny Nz e
546 let tv := ReggeRigorousFoundation.edgeVertices f
547 (canonicalTetVerts Nx Ny Nz τ tv.1 = ev.1 ∧
548 canonicalTetVerts Nx Ny Nz τ tv.2 = ev.2) ∨
549 (canonicalTetVerts Nx Ny Nz τ tv.1 = ev.2 ∧
550 canonicalTetVerts Nx Ny Nz τ tv.2 = ev.1)
551
552theorem localEdgeOf_endpoints_match_tetVerts
553 {Nx Ny Nz : ℕ} [NeZero Nx] [NeZero Ny] [NeZero Nz]
554 (cell : Vertex Nx Ny Nz) (tet f : Fin 6) :
555 let edge := localEdgeOf cell tet f
556 let ev := edge.endpoints
557 let tv := ReggeRigorousFoundation.edgeVertices f
558 (addVertexBits cell (FreudenthalCubeTriangulation.tetVerts tet tv.1) = ev.1 ∧
559 addVertexBits cell (FreudenthalCubeTriangulation.tetVerts tet tv.2) = ev.2) ∨
560 (addVertexBits cell (FreudenthalCubeTriangulation.tetVerts tet tv.1) = ev.2 ∧
561 addVertexBits cell (FreudenthalCubeTriangulation.tetVerts tet tv.2) = ev.1) := by
562 fin_cases tet <;> fin_cases f <;>
563 simp [localEdgeOf, PeriodicEdge.endpoints,
564 FreudenthalCubeTriangulation.localEdgeOf,
565 FreudenthalCubeTriangulation.tetVerts,
566 ReggeRigorousFoundation.edgeVertices,
567 cubeEdgeBase, cubeEdgeDisp, dispBits, vertexBits, addVertexBits, addBits]
568
569theorem canonicalPeriodicEndpointIncidence
570 (Nx Ny Nz : ℕ) [NeZero Nx] [NeZero Ny] [NeZero Nz] :
571 CanonicalPeriodicEndpointIncidence Nx Ny Nz := by
572 intro e τ f h
573 have he := canonicalEdgeInTet_eq_some_implies Nx Ny Nz e τ h
574 let cell := (tetFinEquiv Nx Ny Nz τ).1
575 let tet := (tetFinEquiv Nx Ny Nz τ).2
576 have hlocal := localEdgeOf_endpoints_match_tetVerts (Nx := Nx) (Ny := Ny) (Nz := Nz)
577 cell tet f
578 dsimp [CanonicalPeriodicEndpointIncidence, canonicalEdgeVerts, canonicalTetVerts]
579 rw [he]
580 rcases hlocal with hdir | hrev
581 · left
582 constructor
583 · exact congrArg (vertexFinEquiv Nx Ny Nz).symm hdir.1
584 · exact congrArg (vertexFinEquiv Nx Ny Nz).symm hdir.2
585 · right
586 constructor
587 · exact congrArg (vertexFinEquiv Nx Ny Nz).symm hrev.1
588 · exact congrArg (vertexFinEquiv Nx Ny Nz).symm hrev.2
589
590def canonicalPeriodicIncidenceConsistent_of_endpoint
591 (Nx Ny Nz : ℕ) [NeZero Nx] [NeZero Ny] [NeZero Nz]
592 (hEndpoint : CanonicalPeriodicEndpointIncidence Nx Ny Nz) :
593 IncidenceConsistent (canonicalPeriodicTriangulation Nx Ny Nz) where
594 globalSqEdge := canonicalGlobalSqEdge Nx Ny Nz
595 edgeInTet_vertices := by
596 intro e τ f h
597 exact hEndpoint e τ f h
598 local_sqEdge_eq_global := by
599 intro e τ f h
600 exact canonicalLocalSqEdge_eq_global Nx Ny Nz e τ f h
601 localEdge_complete := by
602 intro τ f
603 exact canonicalLocalEdge_complete Nx Ny Nz
604 (canonicalPeriodicLocalEdgeNoDup Nx Ny Nz) τ f
605 local_schlaefli := by
606 intro τ
607 exact SchlaefliTetrahedronProof.schlaefliTetrahedronClosedForm
608 FreudenthalCubeTriangulation.freudenthalTet
609
610def canonicalPeriodicIncidenceConsistent
611 (Nx Ny Nz : ℕ) [NeZero Nx] [NeZero Ny] [NeZero Nz] :
612 IncidenceConsistent (canonicalPeriodicTriangulation Nx Ny Nz) :=
613 canonicalPeriodicIncidenceConsistent_of_endpoint Nx Ny Nz
614 (canonicalPeriodicEndpointIncidence Nx Ny Nz)
615
616/-- A finite `Triangulation3D` encoding of the typed periodic Freudenthal
617torus. The side-length hypotheses rule out degenerate `+1 = -1`
618wraparound identifications; the actual finite encoder supplies equivalences
619from `Fin` indices to typed cells and positive-displacement edges. -/
620structure EncodedPeriodicFreudenthalTorus
621 (Nx Ny Nz : ℕ) [NeZero Nx] [NeZero Ny] [NeZero Nz] where
622 side_x_gt_two : 2 < Nx
623 side_y_gt_two : 2 < Ny
624 side_z_gt_two : 2 < Nz
625 K : Triangulation3D
626 hK : IncidenceConsistent K
627 tetEquiv : Fin K.nT ≃ (Vertex Nx Ny Nz × Fin 6)
628 edgeEquiv : Fin K.nE ≃ PeriodicEdge Nx Ny Nz
629 edgeInTet_iff :
630 ∀ e τ f,
631 K.edgeInTet e τ = some f ↔
632 edgeEquiv e =
633 localEdgeOf (tetEquiv τ).1 (tetEquiv τ).2 f
634
635def canonicalEncodedPeriodicFreudenthalTorus_of_incidence
636 (Nx Ny Nz : ℕ) [NeZero Nx] [NeZero Ny] [NeZero Nz]
637 (hx : 2 < Nx) (hy : 2 < Ny) (hz : 2 < Nz)
638 (hK : IncidenceConsistent (canonicalPeriodicTriangulation Nx Ny Nz))
639 (hNoDup : CanonicalPeriodicLocalEdgeNoDup Nx Ny Nz) :
640 EncodedPeriodicFreudenthalTorus Nx Ny Nz where
641 side_x_gt_two := hx
642 side_y_gt_two := hy
643 side_z_gt_two := hz
644 K := canonicalPeriodicTriangulation Nx Ny Nz
645 hK := hK
646 tetEquiv := canonicalPeriodicTetEquiv Nx Ny Nz
647 edgeEquiv := canonicalPeriodicEdgeEquiv Nx Ny Nz
648 edgeInTet_iff := by
649 intro e τ f
650 exact canonicalEdgeInTet_iff_of_noDup Nx Ny Nz hNoDup e τ f
651
652def canonicalEncodedPeriodicFreudenthalTorus_of_endpoint
653 (Nx Ny Nz : ℕ) [NeZero Nx] [NeZero Ny] [NeZero Nz]
654 (hx : 2 < Nx) (hy : 2 < Ny) (hz : 2 < Nz)
655 (hEndpoint : CanonicalPeriodicEndpointIncidence Nx Ny Nz) :
656 EncodedPeriodicFreudenthalTorus Nx Ny Nz :=
657 canonicalEncodedPeriodicFreudenthalTorus_of_incidence Nx Ny Nz hx hy hz
658 (canonicalPeriodicIncidenceConsistent_of_endpoint Nx Ny Nz hEndpoint)
659 (canonicalPeriodicLocalEdgeNoDup Nx Ny Nz)
660
661def canonicalEncodedPeriodicFreudenthalTorus
662 (Nx Ny Nz : ℕ) [NeZero Nx] [NeZero Ny] [NeZero Nz]
663 (hx : 2 < Nx) (hy : 2 < Ny) (hz : 2 < Nz) :
664 EncodedPeriodicFreudenthalTorus Nx Ny Nz :=
665 canonicalEncodedPeriodicFreudenthalTorus_of_endpoint Nx Ny Nz hx hy hz
666 (canonicalPeriodicEndpointIncidence Nx Ny Nz)
667
668theorem canonicalEncodedPeriodic_K_tetVerts_eq
669 (Nx Ny Nz : ℕ) [NeZero Nx] [NeZero Ny] [NeZero Nz]
670 (hx : 2 < Nx) (hy : 2 < Ny) (hz : 2 < Nz)
671 (τ : Fin (Fintype.card (PeriodicTet Nx Ny Nz))) (k : Fin 4) :
672 (canonicalEncodedPeriodicFreudenthalTorus Nx Ny Nz hx hy hz).K.tetVerts τ k =
673 canonicalTetVerts Nx Ny Nz τ k := by
674 dsimp [canonicalEncodedPeriodicFreudenthalTorus, canonicalEncodedPeriodicFreudenthalTorus_of_endpoint,
675 canonicalEncodedPeriodicFreudenthalTorus_of_incidence, canonicalPeriodicTriangulation]
676
677theorem canonicalEncodedPeriodic_tetEquiv_eq
678 (Nx Ny Nz : ℕ) [NeZero Nx] [NeZero Ny] [NeZero Nz]
679 (hx : 2 < Nx) (hy : 2 < Ny) (hz : 2 < Nz) :
680 (canonicalEncodedPeriodicFreudenthalTorus Nx Ny Nz hx hy hz).tetEquiv =
681 canonicalPeriodicTetEquiv Nx Ny Nz := by
682 dsimp [canonicalEncodedPeriodicFreudenthalTorus, canonicalEncodedPeriodicFreudenthalTorus_of_endpoint,
683 canonicalEncodedPeriodicFreudenthalTorus_of_incidence, canonicalPeriodicTetEquiv]
684
685theorem canonicalEncodedPeriodic_tetVerts_addVertexBits
686 (Nx Ny Nz : ℕ) [NeZero Nx] [NeZero Ny] [NeZero Nz]
687 (hx : 2 < Nx) (hy : 2 < Ny) (hz : 2 < Nz)
688 (cell : Vertex Nx Ny Nz) (tet : Fin 6) (v : Fin 4) :
689 (canonicalEncodedPeriodicFreudenthalTorus Nx Ny Nz hx hy hz).K.tetVerts
690 ((canonicalEncodedPeriodicFreudenthalTorus Nx Ny Nz hx hy hz).tetEquiv.symm (cell, tet)) v =
691 (vertexFinEquiv Nx Ny Nz).symm
692 (addVertexBits cell (FreudenthalCubeTriangulation.tetVerts tet v)) := by
693 rw [canonicalEncodedPeriodic_tetEquiv_eq, canonicalEncodedPeriodic_K_tetVerts_eq]
694 dsimp only [canonicalTetVerts, canonicalPeriodicTetEquiv]
695 generalize hdef : (tetFinEquiv Nx Ny Nz) ((tetFinEquiv Nx Ny Nz).symm (cell, tet)) = cellTet
696 have hcellTet : cellTet = (cell, tet) :=
697 hdef.symm.trans ((tetFinEquiv Nx Ny Nz).apply_symm_apply (cell, tet))
698 rw [hcellTet]
699
700def edgeSlotPartition_of_encodedPeriodicFreudenthalTorus
701 {Nx Ny Nz : ℕ} [NeZero Nx] [NeZero Ny] [NeZero Nz]
702 (P : EncodedPeriodicFreudenthalTorus Nx Ny Nz) :
703 IncidenceEdgeSlotPartition P.K P.hK where
704 localEdgeOf := fun τ f =>
705 P.edgeEquiv.symm (localEdgeOf (P.tetEquiv τ).1 (P.tetEquiv τ).2 f)
706 edgeInTet_iff := by
707 intro e τ f
708 constructor
709 · intro h
710 apply P.edgeEquiv.injective
711 simpa using (P.edgeInTet_iff e τ f).1 h
712 · intro h
713 apply (P.edgeInTet_iff e τ f).2
714 rw [h]
715 simp
716
717def edgeSlotBookkeeping_of_encodedPeriodicFreudenthalTorus
718 {Nx Ny Nz : ℕ} [NeZero Nx] [NeZero Ny] [NeZero Nz]
719 (P : EncodedPeriodicFreudenthalTorus Nx Ny Nz) :
720 IncidenceEdgeSlotBookkeeping P.K P.hK :=
721 incidenceEdgeSlotBookkeeping_of_partition P.K P.hK
722 (edgeSlotPartition_of_encodedPeriodicFreudenthalTorus P)
723
724end
725
726end PeriodicFreudenthalTorus
727end Geometry
728end IndisputableMonolith
729