IndisputableMonolith.Geometry.PeriodicFreudenthalTorus4D
IndisputableMonolith/Geometry/PeriodicFreudenthalTorus4D.lean · 1403 lines · 69 declarations
show as:
view math explainer →
1import Mathlib
2
3/-!
4# Periodic Freudenthal 4-Torus: the typed 4D carrier
5
6This module builds the typed periodic Freudenthal triangulation of the
74-torus that the 4D `MetricRefinementFamily` recon
8(`QG/attack_full_theory_20260729/A23_4D_recon_20260729.html`) named as the
9missing object: four-coordinate periodic vertices, the fifteen
10positive-displacement edge classes of the 4-cube, the Kuhn (permutation)
11triangulation of the 4-cube into `4! = 24` four-simplices, a finite encoder,
12a self-contained simplicial carrier with simpliciality evidence, and the
13mesh scale machinery.
14
15It is the 4D mirror of `Geometry/PeriodicFreudenthalTorus.lean` (3D). Per the
16recon, it is deliberately self-contained: `PathSumMeasure.BoundedComplex` is
17tetrahedron-only and cannot hold Kuhn 4-simplices (`Fin 5` corners), so this
18module defines its own carrier shape `Carrier4D` and its own simplicial
19predicate `IsSimplicial4D` mirroring the 3D interface. Extending
20`BoundedComplex` to admit 4-simplices is a separate authorized decision and
21is not taken here. No existing module is modified.
22
23Honesty boundary:
24* THEOREM: every named result below (kernel-checked, no `sorry`, no new
25 axioms, no `native_decide`). Finite combinatorial checks on explicit tables
26 use `decide` only.
27* The Kuhn tables are explicit: corners are the partial sums of the 24
28 permutations of the four axes (lexicographic order), and every edge slot is
29 a comparable corner pair. The kernel re-verifies the tables through the
30 endpoint-incidence theorem `localEdgeOf4_endpoints_match_kuhnVerts`.
31* What is NOT here: the side schedule, Config, coarsen, decoration pullback,
32 action step control, and the `MetricRefinementFamily` instance itself.
33 Those are the next worker's assembly job (the 4D analog of
34 `Gap2MetricRefinementFamilyInstance`); the period-doubling projection and
35 its section live in `Gravity/SevenGaps/Gap2FreudenthalPeriodDoubling4D`.
36
37Expected axiom footprint: `[propext, Classical.choice, Quot.sound]`.
38-/
39
40namespace IndisputableMonolith
41namespace Geometry
42namespace PeriodicFreudenthalTorus4D
43
44noncomputable section
45
46/-! ## §1. One-coordinate bit arithmetic (self-contained mirror of the 3D helpers) -/
47
48def bit : Bool → ℕ
49 | false => 0
50 | true => 1
51
52def addBit {N : ℕ} [NeZero N] (i : Fin N) (b : Bool) : Fin N :=
53 ⟨(i.val + bit b) % N, Nat.mod_lt _ (Nat.pos_of_neZero N)⟩
54
55@[simp] theorem addBit_false {N : ℕ} [NeZero N] (i : Fin N) :
56 addBit i false = i := by
57 ext
58 simp [addBit, bit, Nat.mod_eq_of_lt i.isLt]
59
60@[simp] theorem addBit_true_eq_mk {N : ℕ} [NeZero N] (i : Fin N) :
61 addBit i true =
62 ⟨(i.val + 1) % N, Nat.mod_lt _ (Nat.pos_of_neZero N)⟩ := by
63 rfl
64
65@[simp] theorem addBit_false_after_true {N : ℕ} [NeZero N] (i : Fin N) :
66 addBit (addBit i true) false = addBit i true := by
67 simp
68
69@[simp] theorem addBit_true_after_false {N : ℕ} [NeZero N] (i : Fin N) :
70 addBit (addBit i false) true = addBit i true := by
71 simp
72
73theorem addBit_true_ne_self {N : ℕ} [NeZero N] (hN : 2 < N) (i : Fin N) :
74 addBit i true ≠ i := by
75 intro h
76 have hval : (i.val + 1) % N = i.val := by
77 simpa [addBit, bit] using congrArg Fin.val h
78 have hcases : i.val + 1 < N ∨ i.val + 1 = N := by
79 omega
80 cases hcases with
81 | inl hlt =>
82 have hmod : (i.val + 1) % N = i.val + 1 := Nat.mod_eq_of_lt hlt
83 omega
84 | inr heq =>
85 have hmod : (i.val + 1) % N = 0 := by
86 rw [heq, Nat.mod_self]
87 omega
88
89theorem addBit_true_injective {N : ℕ} [NeZero N] :
90 Function.Injective (fun i : Fin N => addBit i true) := by
91 intro i j h
92 ext
93 have hval : (i.val + 1) % N = (j.val + 1) % N := by
94 simpa [addBit, bit] using congrArg Fin.val h
95 have hi : i.val + 1 < N ∨ i.val + 1 = N := by
96 omega
97 have hj : j.val + 1 < N ∨ j.val + 1 = N := by
98 omega
99 cases hi with
100 | inl hi_lt =>
101 have himod : (i.val + 1) % N = i.val + 1 := Nat.mod_eq_of_lt hi_lt
102 cases hj with
103 | inl hj_lt =>
104 have hjmod : (j.val + 1) % N = j.val + 1 := Nat.mod_eq_of_lt hj_lt
105 omega
106 | inr hj_eq =>
107 have hjmod : (j.val + 1) % N = 0 := by
108 rw [hj_eq, Nat.mod_self]
109 omega
110 | inr hi_eq =>
111 have himod : (i.val + 1) % N = 0 := by
112 rw [hi_eq, Nat.mod_self]
113 cases hj with
114 | inl hj_lt =>
115 have hjmod : (j.val + 1) % N = j.val + 1 := Nat.mod_eq_of_lt hj_lt
116 omega
117 | inr hj_eq =>
118 omega
119
120theorem addBit_injective {N : ℕ} [NeZero N] (b : Bool) :
121 Function.Injective (fun i : Fin N => addBit i b) := by
122 cases b
123 · intro i j h
124 simpa using h
125 · exact addBit_true_injective
126
127/-- If two one-step bit translations of the same coordinate agree, the bits
128agree when `1 < N`. (4D copy of the 3D cancellation lemma.) -/
129theorem addBit4_cancel (N : ℕ) [NeZero N] (hN : 1 < N)
130 (c : Fin N) (b₁ b₂ : Bool) (h : addBit c b₁ = addBit c b₂) : b₁ = b₂ := by
131 have hval : (c.val + bit b₁) % N = (c.val + bit b₂) % N := by
132 simpa [addBit] using congrArg Fin.val h
133 have h' : (c.val % N + bit b₁) % N = (c.val % N + bit b₂) % N := by
134 simpa [Nat.add_mod] using hval
135 have hc : c.val % N = c.val := Nat.mod_eq_of_lt c.isLt
136 rw [hc] at h'
137 cases b₁ <;> cases b₂ <;> simp [bit] at h' ⊢
138 · have hcases : c.val + 1 < N ∨ c.val + 1 = N := by omega
139 cases hcases with
140 | inl hlt =>
141 have : (c.val + 1) % N = c.val + 1 := Nat.mod_eq_of_lt hlt
142 omega
143 | inr heq =>
144 have : (c.val + 1) % N = 0 := by rw [heq, Nat.mod_self]
145 omega
146 · have hcases : c.val + 1 < N ∨ c.val + 1 = N := by omega
147 cases hcases with
148 | inl hlt =>
149 have : (c.val + 1) % N = c.val + 1 := Nat.mod_eq_of_lt hlt
150 omega
151 | inr heq =>
152 have : (c.val + 1) % N = 0 := by rw [heq, Nat.mod_self]
153 omega
154
155private theorem two_bit_steps_ne_id (N : ℕ) [NeZero N] (hN : 2 < N)
156 (x : Fin N) (b₁ b₂ : Bool) :
157 addBit (addBit x b₁) b₂ = x → b₁ = false ∧ b₂ = false := by
158 intro h
159 cases b₁ <;> cases b₂
160 · simp [addBit_false] at h ⊢
161 · exact (addBit_true_ne_self hN x (by simpa [addBit_false] using h)).elim
162 · exact (addBit_true_ne_self hN x (by simpa [addBit_false] using h)).elim
163 · have hv : ((x.val + 1) % N + 1) % N = x.val := by
164 simpa [addBit, bit] using congrArg Fin.val h
165 have : x.val + 1 < N ∨ x.val + 1 = N := by omega
166 cases this with
167 | inl hlt =>
168 rw [Nat.mod_eq_of_lt hlt] at hv
169 have hv' : (x.val + 2) % N = x.val := by simpa [Nat.add_assoc] using hv
170 have : x.val + 2 < N ∨ x.val + 2 = N := by omega
171 cases this with
172 | inl hlt2 =>
173 have : x.val + 2 = x.val := by rwa [Nat.mod_eq_of_lt hlt2] at hv'
174 omega
175 | inr heq2 =>
176 have : (x.val + 2) % N = 0 := by rw [heq2, Nat.mod_self]
177 omega
178 | inr heq =>
179 rw [heq, Nat.mod_self] at hv
180 have h1 : 1 % N = 1 := Nat.mod_eq_of_lt (lt_trans (by decide : 1 < 2) hN)
181 rw [h1] at hv
182 omega
183
184/-! ## §2. Periodic 4-grid vertices -/
185
186/-- Periodic 4-torus vertices on the side-`N` grid. -/
187abbrev Vertex4 (N : ℕ) := Fin N × Fin N × Fin N × Fin N
188
189/-- Four-axis bit translation of a periodic vertex. -/
190def addBits4 {N : ℕ} [NeZero N] (v : Vertex4 N) (dx dy dz dw : Bool) : Vertex4 N :=
191 (addBit v.1 dx, addBit v.2.1 dy, addBit v.2.2.1 dz, addBit v.2.2.2 dw)
192
193theorem addBits4_injective {N : ℕ} [NeZero N] (dx dy dz dw : Bool) :
194 Function.Injective (fun v : Vertex4 N => addBits4 v dx dy dz dw) := by
195 intro v w h
196 rcases v with ⟨vx, vy, vz, vw⟩
197 rcases w with ⟨wx, wy, wz, ww⟩
198 simp [addBits4] at h ⊢
199 exact ⟨addBit_injective dx h.1, addBit_injective dy h.2.1,
200 addBit_injective dz h.2.2.1, addBit_injective dw h.2.2.2⟩
201
202/-- Equality of two four-axis bit translations cancels to equality of the
203bits, when `1 < N`. -/
204theorem addBits4_cancel_offsets (N : ℕ) [NeZero N] (hN : 1 < N)
205 (cell : Vertex4 N) (dx₁ dy₁ dz₁ dw₁ dx₂ dy₂ dz₂ dw₂ : Bool)
206 (h : addBits4 cell dx₁ dy₁ dz₁ dw₁ = addBits4 cell dx₂ dy₂ dz₂ dw₂) :
207 dx₁ = dx₂ ∧ dy₁ = dy₂ ∧ dz₁ = dz₂ ∧ dw₁ = dw₂ :=
208 ⟨addBit4_cancel N hN cell.1 dx₁ dx₂ (congrArg Prod.fst h),
209 addBit4_cancel N hN cell.2.1 dy₁ dy₂
210 (congrArg (fun v : Vertex4 N => v.2.1) h),
211 addBit4_cancel N hN cell.2.2.1 dz₁ dz₂
212 (congrArg (fun v : Vertex4 N => v.2.2.1) h),
213 addBit4_cancel N hN cell.2.2.2 dw₁ dw₂
214 (congrArg (fun v : Vertex4 N => v.2.2.2) h)⟩
215
216/-! ## §3. The fifteen positive-displacement classes of the 4-cube -/
217
218/-- Nonzero positive 4-cube displacements, ordered by the bit mask
219`d.val + 1` (bit `i` of the mask is coordinate `i`). The weight spectrum is
220four axis edges (classes 0, 1, 3, 7), six face diagonals (2, 4, 5, 8, 9, 11),
221four space diagonals of 3-faces (6, 10, 12, 13), and one hyperbody diagonal
222(14). Matches the `ReggeEdgeStencil4D` mask convention; the bit-for-bit
223bridge is proved in `Gap2FreudenthalPeriodDoubling4D`. -/
224def dispBits4 : Fin 15 → Bool × Bool × Bool × Bool
225 | 0 => (true, false, false, false)
226 | 1 => (false, true, false, false)
227 | 2 => (true, true, false, false)
228 | 3 => (false, false, true, false)
229 | 4 => (true, false, true, false)
230 | 5 => (false, true, true, false)
231 | 6 => (true, true, true, false)
232 | 7 => (false, false, false, true)
233 | 8 => (true, false, false, true)
234 | 9 => (false, true, false, true)
235 | 10 => (true, true, false, true)
236 | 11 => (false, false, true, true)
237 | 12 => (true, false, true, true)
238 | 13 => (false, true, true, true)
239 | 14 => (true, true, true, true)
240
241theorem dispBits4_ne_zero (d : Fin 15) :
242 dispBits4 d ≠ (false, false, false, false) := by
243 revert d
244 decide
245
246theorem dispBits4_injective : Function.Injective dispBits4 := by
247 decide
248
249/-- **Sanity (displacement classes).** The edge displacement classes are
250exactly fifteen: `dispBits4` is a bijection between `Fin 15` and the nonzero
2510/1 displacement vectors of the 4-cube. -/
252theorem displacement_classes_are_fifteen :
253 Function.Injective dispBits4 ∧
254 (∀ d : Fin 15, dispBits4 d ≠ (false, false, false, false)) ∧
255 (∀ b : Bool × Bool × Bool × Bool, b ≠ (false, false, false, false) →
256 ∃ d : Fin 15, dispBits4 d = b) := by
257 decide
258
259/-! ## §4. Local 4-cube vertex offsets -/
260
261/-- Local 4-cube vertex offsets, using binary cube labels (`Fin 16`, bit `i`
262of the label is coordinate `i`). -/
263def vertexBits4 : Fin 16 → Bool × Bool × Bool × Bool
264 | 0 => (false, false, false, false)
265 | 1 => (true, false, false, false)
266 | 2 => (false, true, false, false)
267 | 3 => (true, true, false, false)
268 | 4 => (false, false, true, false)
269 | 5 => (true, false, true, false)
270 | 6 => (false, true, true, false)
271 | 7 => (true, true, true, false)
272 | 8 => (false, false, false, true)
273 | 9 => (true, false, false, true)
274 | 10 => (false, true, false, true)
275 | 11 => (true, true, false, true)
276 | 12 => (false, false, true, true)
277 | 13 => (true, false, true, true)
278 | 14 => (false, true, true, true)
279 | ⟨_+15, _⟩ => (true, true, true, true)
280
281theorem vertexBits4_injective : Function.Injective vertexBits4 := by
282 decide
283
284/-- Translate a periodic vertex by a local 4-cube corner offset. -/
285def addVertexBits4 {N : ℕ} [NeZero N] (v : Vertex4 N) (a : Fin 16) : Vertex4 N :=
286 let b := vertexBits4 a
287 addBits4 v b.1 b.2.1 b.2.2.1 b.2.2.2
288
289theorem addVertexBits4_injective {N : ℕ} [NeZero N] (a : Fin 16) :
290 Function.Injective (fun v : Vertex4 N => addVertexBits4 v a) := by
291 intro v w h
292 unfold addVertexBits4 at h
293 exact addBits4_injective _ _ _ _ h
294
295/-! ## §5. Positive-displacement periodic 4-edges -/
296
297/-- A positive-displacement periodic 4-edge, represented by its base vertex
298and one of the fifteen positive 4-cube displacement classes. -/
299structure PeriodicEdge4 (N : ℕ) [NeZero N] where
300 base : Vertex4 N
301 disp : Fin 15
302deriving DecidableEq, Fintype
303
304/-- Endpoints of a positive-displacement periodic 4-edge. -/
305def PeriodicEdge4.endpoints {N : ℕ} [NeZero N] (e : PeriodicEdge4 N) :
306 Vertex4 N × Vertex4 N :=
307 let d := dispBits4 e.disp
308 (e.base, addBits4 e.base d.1 d.2.1 d.2.2.1 d.2.2.2)
309
310theorem PeriodicEdge4.endpoints_ne {N : ℕ} [NeZero N] (hN : 2 < N)
311 (e : PeriodicEdge4 N) :
312 e.endpoints.1 ≠ e.endpoints.2 := by
313 cases e with
314 | mk base disp =>
315 fin_cases disp <;>
316 · intro h
317 simp [PeriodicEdge4.endpoints, dispBits4, addBits4] at h
318 first
319 | exact addBit_true_ne_self hN base.1 ((congrArg Prod.fst h).symm)
320 | exact addBit_true_ne_self hN base.2.1
321 ((congrArg (fun v : Vertex4 N => v.2.1) h).symm)
322 | exact addBit_true_ne_self hN base.2.2.1
323 ((congrArg (fun v : Vertex4 N => v.2.2.1) h).symm)
324 | exact addBit_true_ne_self hN base.2.2.2
325 ((congrArg (fun v : Vertex4 N => v.2.2.2) h).symm)
326
327/-! ## §6. Cardinalities of the typed skeleton -/
328
329/-- The periodic 4-vertex set at side `N` has `N ^ 4` elements. -/
330theorem card_vertex4 (N : ℕ) : Fintype.card (Vertex4 N) = N ^ 4 := by
331 rw [Fintype.card_prod, Fintype.card_prod, Fintype.card_prod, Fintype.card_fin]
332 ring
333
334/-- A positive-displacement periodic 4-edge is exactly a (base vertex,
335displacement class) pair. -/
336def periodicEdge4EquivProd (N : ℕ) [NeZero N] :
337 PeriodicEdge4 N ≃ Vertex4 N × Fin 15 where
338 toFun e := (e.base, e.disp)
339 invFun p := ⟨p.1, p.2⟩
340 left_inv _ := rfl
341 right_inv _ := rfl
342
343/-- **Edge count formula.** The periodic 4-edge set at side `N` has
344`15 * N ^ 4` elements. -/
345theorem card_periodicEdge4 (N : ℕ) [NeZero N] :
346 Fintype.card (PeriodicEdge4 N) = 15 * N ^ 4 := by
347 rw [Fintype.card_congr (periodicEdge4EquivProd N), Fintype.card_prod,
348 card_vertex4, Fintype.card_fin]
349 ring
350
351/- Finite types of the carrier: vertices and edges (and below, Kuhn
352simplices) are finite at every side, by the derived `Fintype` instances on
353`Vertex4` (a product of `Fin`) and `PeriodicEdge4` (`deriving Fintype`). -/
354
355/-! ## §7. The Kuhn triangulation of the 4-cube (24 permutation simplices) -/
356
357/-- The 24 Kuhn 4-simplices of the unit 4-cube as corner lists: the monotone
358paths from cube vertex `0` to cube vertex `15`, one per permutation of the
359four axes, in lexicographic permutation order. Corner `k` of simplex `σ` is
360the partial sum of the first `k` axis steps, as a binary cube label. -/
361def kuhnVerts : Fin 24 → Fin 5 → Fin 16
362 | 0, 0 => 0
363 | 0, 1 => 1
364 | 0, 2 => 3
365 | 0, 3 => 7
366 | 0, 4 => 15
367 | 1, 0 => 0
368 | 1, 1 => 1
369 | 1, 2 => 3
370 | 1, 3 => 11
371 | 1, 4 => 15
372 | 2, 0 => 0
373 | 2, 1 => 1
374 | 2, 2 => 5
375 | 2, 3 => 7
376 | 2, 4 => 15
377 | 3, 0 => 0
378 | 3, 1 => 1
379 | 3, 2 => 5
380 | 3, 3 => 13
381 | 3, 4 => 15
382 | 4, 0 => 0
383 | 4, 1 => 1
384 | 4, 2 => 9
385 | 4, 3 => 11
386 | 4, 4 => 15
387 | 5, 0 => 0
388 | 5, 1 => 1
389 | 5, 2 => 9
390 | 5, 3 => 13
391 | 5, 4 => 15
392 | 6, 0 => 0
393 | 6, 1 => 2
394 | 6, 2 => 3
395 | 6, 3 => 7
396 | 6, 4 => 15
397 | 7, 0 => 0
398 | 7, 1 => 2
399 | 7, 2 => 3
400 | 7, 3 => 11
401 | 7, 4 => 15
402 | 8, 0 => 0
403 | 8, 1 => 2
404 | 8, 2 => 6
405 | 8, 3 => 7
406 | 8, 4 => 15
407 | 9, 0 => 0
408 | 9, 1 => 2
409 | 9, 2 => 6
410 | 9, 3 => 14
411 | 9, 4 => 15
412 | 10, 0 => 0
413 | 10, 1 => 2
414 | 10, 2 => 10
415 | 10, 3 => 11
416 | 10, 4 => 15
417 | 11, 0 => 0
418 | 11, 1 => 2
419 | 11, 2 => 10
420 | 11, 3 => 14
421 | 11, 4 => 15
422 | 12, 0 => 0
423 | 12, 1 => 4
424 | 12, 2 => 5
425 | 12, 3 => 7
426 | 12, 4 => 15
427 | 13, 0 => 0
428 | 13, 1 => 4
429 | 13, 2 => 5
430 | 13, 3 => 13
431 | 13, 4 => 15
432 | 14, 0 => 0
433 | 14, 1 => 4
434 | 14, 2 => 6
435 | 14, 3 => 7
436 | 14, 4 => 15
437 | 15, 0 => 0
438 | 15, 1 => 4
439 | 15, 2 => 6
440 | 15, 3 => 14
441 | 15, 4 => 15
442 | 16, 0 => 0
443 | 16, 1 => 4
444 | 16, 2 => 12
445 | 16, 3 => 13
446 | 16, 4 => 15
447 | 17, 0 => 0
448 | 17, 1 => 4
449 | 17, 2 => 12
450 | 17, 3 => 14
451 | 17, 4 => 15
452 | 18, 0 => 0
453 | 18, 1 => 8
454 | 18, 2 => 9
455 | 18, 3 => 11
456 | 18, 4 => 15
457 | 19, 0 => 0
458 | 19, 1 => 8
459 | 19, 2 => 9
460 | 19, 3 => 13
461 | 19, 4 => 15
462 | 20, 0 => 0
463 | 20, 1 => 8
464 | 20, 2 => 10
465 | 20, 3 => 11
466 | 20, 4 => 15
467 | 21, 0 => 0
468 | 21, 1 => 8
469 | 21, 2 => 10
470 | 21, 3 => 14
471 | 21, 4 => 15
472 | 22, 0 => 0
473 | 22, 1 => 8
474 | 22, 2 => 12
475 | 22, 3 => 13
476 | 22, 4 => 15
477 | 23, 0 => 0
478 | 23, 1 => 8
479 | 23, 2 => 12
480 | 23, 3 => 14
481 | 23, 4 => 15
482 | ⟨n+24, h⟩, _ => absurd h (by omega)
483
484/-- The ten edge slots of a 4-simplex: corner pairs `(i, j)` with `i < j`,
485in lexicographic order. -/
486def edgeSlotPair : Fin 10 → Fin 5 × Fin 5
487 | 0 => (0, 1)
488 | 1 => (0, 2)
489 | 2 => (0, 3)
490 | 3 => (0, 4)
491 | 4 => (1, 2)
492 | 5 => (1, 3)
493 | 6 => (1, 4)
494 | 7 => (2, 3)
495 | 8 => (2, 4)
496 | 9 => (3, 4)
497 | ⟨n+10, h⟩ => absurd h (by omega)
498
499/-- Base cube-corner label of each Kuhn edge slot: slot `f` of simplex `σ`
500starts at corner `(edgeSlotPair f).1`. -/
501def kuhnEdgeBase : Fin 24 → Fin 10 → Fin 16
502 | 0, 0 => 0
503 | 0, 1 => 0
504 | 0, 2 => 0
505 | 0, 3 => 0
506 | 0, 4 => 1
507 | 0, 5 => 1
508 | 0, 6 => 1
509 | 0, 7 => 3
510 | 0, 8 => 3
511 | 0, 9 => 7
512 | 1, 0 => 0
513 | 1, 1 => 0
514 | 1, 2 => 0
515 | 1, 3 => 0
516 | 1, 4 => 1
517 | 1, 5 => 1
518 | 1, 6 => 1
519 | 1, 7 => 3
520 | 1, 8 => 3
521 | 1, 9 => 11
522 | 2, 0 => 0
523 | 2, 1 => 0
524 | 2, 2 => 0
525 | 2, 3 => 0
526 | 2, 4 => 1
527 | 2, 5 => 1
528 | 2, 6 => 1
529 | 2, 7 => 5
530 | 2, 8 => 5
531 | 2, 9 => 7
532 | 3, 0 => 0
533 | 3, 1 => 0
534 | 3, 2 => 0
535 | 3, 3 => 0
536 | 3, 4 => 1
537 | 3, 5 => 1
538 | 3, 6 => 1
539 | 3, 7 => 5
540 | 3, 8 => 5
541 | 3, 9 => 13
542 | 4, 0 => 0
543 | 4, 1 => 0
544 | 4, 2 => 0
545 | 4, 3 => 0
546 | 4, 4 => 1
547 | 4, 5 => 1
548 | 4, 6 => 1
549 | 4, 7 => 9
550 | 4, 8 => 9
551 | 4, 9 => 11
552 | 5, 0 => 0
553 | 5, 1 => 0
554 | 5, 2 => 0
555 | 5, 3 => 0
556 | 5, 4 => 1
557 | 5, 5 => 1
558 | 5, 6 => 1
559 | 5, 7 => 9
560 | 5, 8 => 9
561 | 5, 9 => 13
562 | 6, 0 => 0
563 | 6, 1 => 0
564 | 6, 2 => 0
565 | 6, 3 => 0
566 | 6, 4 => 2
567 | 6, 5 => 2
568 | 6, 6 => 2
569 | 6, 7 => 3
570 | 6, 8 => 3
571 | 6, 9 => 7
572 | 7, 0 => 0
573 | 7, 1 => 0
574 | 7, 2 => 0
575 | 7, 3 => 0
576 | 7, 4 => 2
577 | 7, 5 => 2
578 | 7, 6 => 2
579 | 7, 7 => 3
580 | 7, 8 => 3
581 | 7, 9 => 11
582 | 8, 0 => 0
583 | 8, 1 => 0
584 | 8, 2 => 0
585 | 8, 3 => 0
586 | 8, 4 => 2
587 | 8, 5 => 2
588 | 8, 6 => 2
589 | 8, 7 => 6
590 | 8, 8 => 6
591 | 8, 9 => 7
592 | 9, 0 => 0
593 | 9, 1 => 0
594 | 9, 2 => 0
595 | 9, 3 => 0
596 | 9, 4 => 2
597 | 9, 5 => 2
598 | 9, 6 => 2
599 | 9, 7 => 6
600 | 9, 8 => 6
601 | 9, 9 => 14
602 | 10, 0 => 0
603 | 10, 1 => 0
604 | 10, 2 => 0
605 | 10, 3 => 0
606 | 10, 4 => 2
607 | 10, 5 => 2
608 | 10, 6 => 2
609 | 10, 7 => 10
610 | 10, 8 => 10
611 | 10, 9 => 11
612 | 11, 0 => 0
613 | 11, 1 => 0
614 | 11, 2 => 0
615 | 11, 3 => 0
616 | 11, 4 => 2
617 | 11, 5 => 2
618 | 11, 6 => 2
619 | 11, 7 => 10
620 | 11, 8 => 10
621 | 11, 9 => 14
622 | 12, 0 => 0
623 | 12, 1 => 0
624 | 12, 2 => 0
625 | 12, 3 => 0
626 | 12, 4 => 4
627 | 12, 5 => 4
628 | 12, 6 => 4
629 | 12, 7 => 5
630 | 12, 8 => 5
631 | 12, 9 => 7
632 | 13, 0 => 0
633 | 13, 1 => 0
634 | 13, 2 => 0
635 | 13, 3 => 0
636 | 13, 4 => 4
637 | 13, 5 => 4
638 | 13, 6 => 4
639 | 13, 7 => 5
640 | 13, 8 => 5
641 | 13, 9 => 13
642 | 14, 0 => 0
643 | 14, 1 => 0
644 | 14, 2 => 0
645 | 14, 3 => 0
646 | 14, 4 => 4
647 | 14, 5 => 4
648 | 14, 6 => 4
649 | 14, 7 => 6
650 | 14, 8 => 6
651 | 14, 9 => 7
652 | 15, 0 => 0
653 | 15, 1 => 0
654 | 15, 2 => 0
655 | 15, 3 => 0
656 | 15, 4 => 4
657 | 15, 5 => 4
658 | 15, 6 => 4
659 | 15, 7 => 6
660 | 15, 8 => 6
661 | 15, 9 => 14
662 | 16, 0 => 0
663 | 16, 1 => 0
664 | 16, 2 => 0
665 | 16, 3 => 0
666 | 16, 4 => 4
667 | 16, 5 => 4
668 | 16, 6 => 4
669 | 16, 7 => 12
670 | 16, 8 => 12
671 | 16, 9 => 13
672 | 17, 0 => 0
673 | 17, 1 => 0
674 | 17, 2 => 0
675 | 17, 3 => 0
676 | 17, 4 => 4
677 | 17, 5 => 4
678 | 17, 6 => 4
679 | 17, 7 => 12
680 | 17, 8 => 12
681 | 17, 9 => 14
682 | 18, 0 => 0
683 | 18, 1 => 0
684 | 18, 2 => 0
685 | 18, 3 => 0
686 | 18, 4 => 8
687 | 18, 5 => 8
688 | 18, 6 => 8
689 | 18, 7 => 9
690 | 18, 8 => 9
691 | 18, 9 => 11
692 | 19, 0 => 0
693 | 19, 1 => 0
694 | 19, 2 => 0
695 | 19, 3 => 0
696 | 19, 4 => 8
697 | 19, 5 => 8
698 | 19, 6 => 8
699 | 19, 7 => 9
700 | 19, 8 => 9
701 | 19, 9 => 13
702 | 20, 0 => 0
703 | 20, 1 => 0
704 | 20, 2 => 0
705 | 20, 3 => 0
706 | 20, 4 => 8
707 | 20, 5 => 8
708 | 20, 6 => 8
709 | 20, 7 => 10
710 | 20, 8 => 10
711 | 20, 9 => 11
712 | 21, 0 => 0
713 | 21, 1 => 0
714 | 21, 2 => 0
715 | 21, 3 => 0
716 | 21, 4 => 8
717 | 21, 5 => 8
718 | 21, 6 => 8
719 | 21, 7 => 10
720 | 21, 8 => 10
721 | 21, 9 => 14
722 | 22, 0 => 0
723 | 22, 1 => 0
724 | 22, 2 => 0
725 | 22, 3 => 0
726 | 22, 4 => 8
727 | 22, 5 => 8
728 | 22, 6 => 8
729 | 22, 7 => 12
730 | 22, 8 => 12
731 | 22, 9 => 13
732 | 23, 0 => 0
733 | 23, 1 => 0
734 | 23, 2 => 0
735 | 23, 3 => 0
736 | 23, 4 => 8
737 | 23, 5 => 8
738 | 23, 6 => 8
739 | 23, 7 => 12
740 | 23, 8 => 12
741 | 23, 9 => 14
742 | ⟨n+24, h⟩, _ => absurd h (by omega)
743
744/-- Displacement class of each Kuhn edge slot: slot `f` of simplex `σ` runs
745from corner `(edgeSlotPair f).1` to corner `(edgeSlotPair f).2`, whose
746componentwise difference is one of the fifteen positive classes. Every one
747of the fifteen classes occurs across the table. -/
748def kuhnEdgeDisp : Fin 24 → Fin 10 → Fin 15
749 | 0, 0 => 0
750 | 0, 1 => 2
751 | 0, 2 => 6
752 | 0, 3 => 14
753 | 0, 4 => 1
754 | 0, 5 => 5
755 | 0, 6 => 13
756 | 0, 7 => 3
757 | 0, 8 => 11
758 | 0, 9 => 7
759 | 1, 0 => 0
760 | 1, 1 => 2
761 | 1, 2 => 10
762 | 1, 3 => 14
763 | 1, 4 => 1
764 | 1, 5 => 9
765 | 1, 6 => 13
766 | 1, 7 => 7
767 | 1, 8 => 11
768 | 1, 9 => 3
769 | 2, 0 => 0
770 | 2, 1 => 4
771 | 2, 2 => 6
772 | 2, 3 => 14
773 | 2, 4 => 3
774 | 2, 5 => 5
775 | 2, 6 => 13
776 | 2, 7 => 1
777 | 2, 8 => 9
778 | 2, 9 => 7
779 | 3, 0 => 0
780 | 3, 1 => 4
781 | 3, 2 => 12
782 | 3, 3 => 14
783 | 3, 4 => 3
784 | 3, 5 => 11
785 | 3, 6 => 13
786 | 3, 7 => 7
787 | 3, 8 => 9
788 | 3, 9 => 1
789 | 4, 0 => 0
790 | 4, 1 => 8
791 | 4, 2 => 10
792 | 4, 3 => 14
793 | 4, 4 => 7
794 | 4, 5 => 9
795 | 4, 6 => 13
796 | 4, 7 => 1
797 | 4, 8 => 5
798 | 4, 9 => 3
799 | 5, 0 => 0
800 | 5, 1 => 8
801 | 5, 2 => 12
802 | 5, 3 => 14
803 | 5, 4 => 7
804 | 5, 5 => 11
805 | 5, 6 => 13
806 | 5, 7 => 3
807 | 5, 8 => 5
808 | 5, 9 => 1
809 | 6, 0 => 1
810 | 6, 1 => 2
811 | 6, 2 => 6
812 | 6, 3 => 14
813 | 6, 4 => 0
814 | 6, 5 => 4
815 | 6, 6 => 12
816 | 6, 7 => 3
817 | 6, 8 => 11
818 | 6, 9 => 7
819 | 7, 0 => 1
820 | 7, 1 => 2
821 | 7, 2 => 10
822 | 7, 3 => 14
823 | 7, 4 => 0
824 | 7, 5 => 8
825 | 7, 6 => 12
826 | 7, 7 => 7
827 | 7, 8 => 11
828 | 7, 9 => 3
829 | 8, 0 => 1
830 | 8, 1 => 5
831 | 8, 2 => 6
832 | 8, 3 => 14
833 | 8, 4 => 3
834 | 8, 5 => 4
835 | 8, 6 => 12
836 | 8, 7 => 0
837 | 8, 8 => 8
838 | 8, 9 => 7
839 | 9, 0 => 1
840 | 9, 1 => 5
841 | 9, 2 => 13
842 | 9, 3 => 14
843 | 9, 4 => 3
844 | 9, 5 => 11
845 | 9, 6 => 12
846 | 9, 7 => 7
847 | 9, 8 => 8
848 | 9, 9 => 0
849 | 10, 0 => 1
850 | 10, 1 => 9
851 | 10, 2 => 10
852 | 10, 3 => 14
853 | 10, 4 => 7
854 | 10, 5 => 8
855 | 10, 6 => 12
856 | 10, 7 => 0
857 | 10, 8 => 4
858 | 10, 9 => 3
859 | 11, 0 => 1
860 | 11, 1 => 9
861 | 11, 2 => 13
862 | 11, 3 => 14
863 | 11, 4 => 7
864 | 11, 5 => 11
865 | 11, 6 => 12
866 | 11, 7 => 3
867 | 11, 8 => 4
868 | 11, 9 => 0
869 | 12, 0 => 3
870 | 12, 1 => 4
871 | 12, 2 => 6
872 | 12, 3 => 14
873 | 12, 4 => 0
874 | 12, 5 => 2
875 | 12, 6 => 10
876 | 12, 7 => 1
877 | 12, 8 => 9
878 | 12, 9 => 7
879 | 13, 0 => 3
880 | 13, 1 => 4
881 | 13, 2 => 12
882 | 13, 3 => 14
883 | 13, 4 => 0
884 | 13, 5 => 8
885 | 13, 6 => 10
886 | 13, 7 => 7
887 | 13, 8 => 9
888 | 13, 9 => 1
889 | 14, 0 => 3
890 | 14, 1 => 5
891 | 14, 2 => 6
892 | 14, 3 => 14
893 | 14, 4 => 1
894 | 14, 5 => 2
895 | 14, 6 => 10
896 | 14, 7 => 0
897 | 14, 8 => 8
898 | 14, 9 => 7
899 | 15, 0 => 3
900 | 15, 1 => 5
901 | 15, 2 => 13
902 | 15, 3 => 14
903 | 15, 4 => 1
904 | 15, 5 => 9
905 | 15, 6 => 10
906 | 15, 7 => 7
907 | 15, 8 => 8
908 | 15, 9 => 0
909 | 16, 0 => 3
910 | 16, 1 => 11
911 | 16, 2 => 12
912 | 16, 3 => 14
913 | 16, 4 => 7
914 | 16, 5 => 8
915 | 16, 6 => 10
916 | 16, 7 => 0
917 | 16, 8 => 2
918 | 16, 9 => 1
919 | 17, 0 => 3
920 | 17, 1 => 11
921 | 17, 2 => 13
922 | 17, 3 => 14
923 | 17, 4 => 7
924 | 17, 5 => 9
925 | 17, 6 => 10
926 | 17, 7 => 1
927 | 17, 8 => 2
928 | 17, 9 => 0
929 | 18, 0 => 7
930 | 18, 1 => 8
931 | 18, 2 => 10
932 | 18, 3 => 14
933 | 18, 4 => 0
934 | 18, 5 => 2
935 | 18, 6 => 6
936 | 18, 7 => 1
937 | 18, 8 => 5
938 | 18, 9 => 3
939 | 19, 0 => 7
940 | 19, 1 => 8
941 | 19, 2 => 12
942 | 19, 3 => 14
943 | 19, 4 => 0
944 | 19, 5 => 4
945 | 19, 6 => 6
946 | 19, 7 => 3
947 | 19, 8 => 5
948 | 19, 9 => 1
949 | 20, 0 => 7
950 | 20, 1 => 9
951 | 20, 2 => 10
952 | 20, 3 => 14
953 | 20, 4 => 1
954 | 20, 5 => 2
955 | 20, 6 => 6
956 | 20, 7 => 0
957 | 20, 8 => 4
958 | 20, 9 => 3
959 | 21, 0 => 7
960 | 21, 1 => 9
961 | 21, 2 => 13
962 | 21, 3 => 14
963 | 21, 4 => 1
964 | 21, 5 => 5
965 | 21, 6 => 6
966 | 21, 7 => 3
967 | 21, 8 => 4
968 | 21, 9 => 0
969 | 22, 0 => 7
970 | 22, 1 => 11
971 | 22, 2 => 12
972 | 22, 3 => 14
973 | 22, 4 => 3
974 | 22, 5 => 4
975 | 22, 6 => 6
976 | 22, 7 => 0
977 | 22, 8 => 2
978 | 22, 9 => 1
979 | 23, 0 => 7
980 | 23, 1 => 11
981 | 23, 2 => 13
982 | 23, 3 => 14
983 | 23, 4 => 3
984 | 23, 5 => 5
985 | 23, 6 => 6
986 | 23, 7 => 1
987 | 23, 8 => 2
988 | 23, 9 => 0
989 | ⟨n+24, h⟩, _ => absurd h (by omega)
990
991/-- Periodic Kuhn 4-simplices: one of the 24 Kuhn simplices inside each
992periodic cubic cell. Finite at every side as a product of finite types. -/
993abbrev PeriodicSimplex4 (N : ℕ) := Vertex4 N × Fin 24
994
995/-- **Simplex count formula.** The periodic Kuhn 4-simplex set at side `N`
996has `24 * N ^ 4` elements. -/
997theorem card_periodicSimplex4 (N : ℕ) :
998 Fintype.card (PeriodicSimplex4 N) = 24 * N ^ 4 := by
999 rw [Fintype.card_prod, card_vertex4, Fintype.card_fin]
1000 ring
1001
1002/-- **Sanity (Kuhn count).** The triangulation of one 4-cube has exactly
1003`4! = 24` four-simplices. -/
1004theorem kuhn_simplex_count_per_cube :
1005 Fintype.card (Fin 24) = 24 ∧ Nat.factorial 4 = 24 :=
1006 ⟨rfl, by decide⟩
1007
1008/-- Every Kuhn simplex starts at the cube origin. -/
1009theorem kuhnVerts_zero (σ : Fin 24) : kuhnVerts σ 0 = 0 := by
1010 fin_cases σ <;> rfl
1011
1012/-- Every Kuhn simplex ends at the opposite cube corner `15`. -/
1013theorem kuhnVerts_four (σ : Fin 24) : kuhnVerts σ 4 = 15 := by
1014 fin_cases σ <;> rfl
1015
1016/-- The five corner labels of each Kuhn simplex are pairwise distinct. -/
1017theorem kuhnVerts_label_injective (σ : Fin 24) :
1018 Function.Injective (kuhnVerts σ) := by
1019 fin_cases σ <;> decide
1020
1021/-- The translated global 4-edge of a local Kuhn edge slot. -/
1022def localEdgeOf4 {N : ℕ} [NeZero N] (cell : Vertex4 N) (σ : Fin 24)
1023 (f : Fin 10) : PeriodicEdge4 N :=
1024 { base := addVertexBits4 cell (kuhnEdgeBase σ f), disp := kuhnEdgeDisp σ f }
1025
1026/-- Corner `k` of Kuhn simplex `σ`, translated to the periodic cell. -/
1027def kuhnCornerAt {N : ℕ} [NeZero N] (cell : Vertex4 N) (σ : Fin 24)
1028 (k : Fin 5) : Vertex4 N :=
1029 addVertexBits4 cell (kuhnVerts σ k)
1030
1031set_option maxHeartbeats 1600000 in
1032/-- **Endpoint incidence (edge-in-class sanity).** Every edge slot of every
1033Kuhn 4-simplex is realized by a positive-displacement periodic 4-edge in one
1034of the fifteen classes: slot `f` runs from corner `(edgeSlotPair f).1` to
1035corner `(edgeSlotPair f).2`, and the endpoints of `localEdgeOf4` agree with
1036those translated corners (in direct order, by construction of the tables). -/
1037theorem localEdgeOf4_endpoints_match_kuhnVerts {N : ℕ} [NeZero N]
1038 (cell : Vertex4 N) (σ : Fin 24) (f : Fin 10) :
1039 (kuhnCornerAt cell σ (edgeSlotPair f).1 = (localEdgeOf4 cell σ f).endpoints.1 ∧
1040 kuhnCornerAt cell σ (edgeSlotPair f).2 = (localEdgeOf4 cell σ f).endpoints.2) ∨
1041 (kuhnCornerAt cell σ (edgeSlotPair f).1 = (localEdgeOf4 cell σ f).endpoints.2 ∧
1042 kuhnCornerAt cell σ (edgeSlotPair f).2 = (localEdgeOf4 cell σ f).endpoints.1) := by
1043 fin_cases σ <;> fin_cases f <;>
1044 simp [localEdgeOf4, PeriodicEdge4.endpoints, kuhnCornerAt, edgeSlotPair,
1045 kuhnVerts, kuhnEdgeBase, kuhnEdgeDisp, addVertexBits4, addBits4,
1046 vertexBits4, dispBits4]
1047
1048/-- On a side-`N` torus with `1 < N`, the five corners of any Kuhn
10494-simplex are pairwise distinct. -/
1050theorem kuhn_corners_injective (N : ℕ) [NeZero N] (hN : 1 < N)
1051 (cell : Vertex4 N) (σ : Fin 24) :
1052 Function.Injective (fun k : Fin 5 => kuhnCornerAt cell σ k) := by
1053 intro a b h
1054 have hcancel :
1055 vertexBits4 (kuhnVerts σ a) = vertexBits4 (kuhnVerts σ b) := by
1056 rcases addBits4_cancel_offsets N hN cell
1057 (vertexBits4 (kuhnVerts σ a)).1
1058 (vertexBits4 (kuhnVerts σ a)).2.1
1059 (vertexBits4 (kuhnVerts σ a)).2.2.1
1060 (vertexBits4 (kuhnVerts σ a)).2.2.2
1061 (vertexBits4 (kuhnVerts σ b)).1
1062 (vertexBits4 (kuhnVerts σ b)).2.1
1063 (vertexBits4 (kuhnVerts σ b)).2.2.1
1064 (vertexBits4 (kuhnVerts σ b)).2.2.2
1065 (by simpa [kuhnCornerAt, addVertexBits4] using h) with ⟨hx, hy, hz, hw⟩
1066 exact Prod.ext hx (Prod.ext hy (Prod.ext hz hw))
1067 exact kuhnVerts_label_injective σ (vertexBits4_injective hcancel)
1068
1069/-- The slot of an unordered corner pair (the inverse of `edgeSlotPair` up
1070to orientation). -/
1071def pairSlot4 (i j : Fin 5) : Fin 10 :=
1072 let a := min i j
1073 let b := max i j
1074 if a = 0 ∧ b = 1 then 0
1075 else if a = 0 ∧ b = 2 then 1
1076 else if a = 0 ∧ b = 3 then 2
1077 else if a = 0 ∧ b = 4 then 3
1078 else if a = 1 ∧ b = 2 then 4
1079 else if a = 1 ∧ b = 3 then 5
1080 else if a = 1 ∧ b = 4 then 6
1081 else if a = 2 ∧ b = 3 then 7
1082 else if a = 2 ∧ b = 4 then 8
1083 else 9
1084
1085theorem pairSlot4_spec (i j : Fin 5) (hij : i ≠ j) :
1086 edgeSlotPair (pairSlot4 i j) = (i, j) ∨
1087 edgeSlotPair (pairSlot4 i j) = (j, i) := by
1088 fin_cases i <;> fin_cases j
1089 all_goals (try exact (hij rfl).elim)
1090 all_goals (first | (left; rfl) | (right; rfl))
1091
1092/-! ## §8. Finite encoder -/
1093
1094/-- Canonical finite index set for periodic 4-vertices. -/
1095noncomputable def vertexFinEquiv4 (N : ℕ) [NeZero N] :
1096 Fin (Fintype.card (Vertex4 N)) ≃ Vertex4 N :=
1097 (Fintype.equivFin (Vertex4 N)).symm
1098
1099/-- Canonical finite index set for positive-displacement periodic 4-edges. -/
1100noncomputable def edgeFinEquiv4 (N : ℕ) [NeZero N] :
1101 Fin (Fintype.card (PeriodicEdge4 N)) ≃ PeriodicEdge4 N :=
1102 (Fintype.equivFin (PeriodicEdge4 N)).symm
1103
1104/-- Canonical finite index set for periodic Kuhn 4-simplices. -/
1105noncomputable def simplexFinEquiv4 (N : ℕ) [NeZero N] :
1106 Fin (Fintype.card (PeriodicSimplex4 N)) ≃ PeriodicSimplex4 N :=
1107 (Fintype.equivFin (PeriodicSimplex4 N)).symm
1108
1109/-- Canonical endpoint map for positive-displacement periodic 4-edges,
1110expressed in the finite vertex index set. -/
1111def canonicalEdgeVerts4 (N : ℕ) [NeZero N]
1112 (e : Fin (Fintype.card (PeriodicEdge4 N))) :
1113 Fin (Fintype.card (Vertex4 N)) × Fin (Fintype.card (Vertex4 N)) :=
1114 let edge := edgeFinEquiv4 N e
1115 let endpoints := edge.endpoints
1116 ((vertexFinEquiv4 N).symm endpoints.1,
1117 (vertexFinEquiv4 N).symm endpoints.2)
1118
1119/-- Canonical 4-simplex corner map for the 24-simplex Kuhn decomposition in
1120every periodic cell. -/
1121def canonicalSimplexVerts4 (N : ℕ) [NeZero N]
1122 (τ : Fin (Fintype.card (PeriodicSimplex4 N))) (k : Fin 5) :
1123 Fin (Fintype.card (Vertex4 N)) :=
1124 let cellS := simplexFinEquiv4 N τ
1125 (vertexFinEquiv4 N).symm (addVertexBits4 cellS.1 (kuhnVerts cellS.2 k))
1126
1127/-! ## §9. The simplicial 4D carrier -/
1128
1129/-- Unordered-pair equality of ordered vertex pairs (local mirror of the 3D
1130`sameUnorderedPair`, which lives in the SevenGaps path-sum layer). -/
1131def sameUnorderedPair4 {n : ℕ} (p q : Fin n × Fin n) : Prop :=
1132 p = q ∨ p = q.swap
1133
1134/-- The self-contained 4D analog of the path-sum `BoundedComplex` incidence
1135shape: vertex count, edge count, 4-simplex count, endpoint incidence, and
1136corner incidence with `Fin 5` corners. `BoundedComplex` is tet-only and
1137cannot hold Kuhn 4-simplices; extending it is a separate decision. -/
1138structure Carrier4D where
1139 nV : ℕ
1140 nE : ℕ
1141 nS : ℕ
1142 edgeVerts : Fin nE → Fin nV × Fin nV
1143 simplexVerts : Fin nS → Fin 5 → Fin nV
1144
1145/-- The simplicial predicate on a 4D carrier (mirror of the 3D
1146`IsSimplicial`): no degenerate edges, no multi-edges, injective 4-simplex
1147corners, and skeleton closure (every corner pair of every 4-simplex is an
1148edge of the carrier). -/
1149def IsSimplicial4D (K : Carrier4D) : Prop :=
1150 (∀ e : Fin K.nE, (K.edgeVerts e).1 ≠ (K.edgeVerts e).2) ∧
1151 (∀ e e' : Fin K.nE,
1152 sameUnorderedPair4 (K.edgeVerts e) (K.edgeVerts e') → e = e') ∧
1153 (∀ s : Fin K.nS, Function.Injective (K.simplexVerts s)) ∧
1154 (∀ (s : Fin K.nS) (i j : Fin 5), i ≠ j →
1155 ∃ e : Fin K.nE,
1156 sameUnorderedPair4 (K.edgeVerts e) (K.simplexVerts s i, K.simplexVerts s j))
1157
1158/-- The canonical periodic Freudenthal 4-torus carrier at side `N`. -/
1159def canonicalCarrier4D (N : ℕ) [NeZero N] : Carrier4D where
1160 nV := Fintype.card (Vertex4 N)
1161 nE := Fintype.card (PeriodicEdge4 N)
1162 nS := Fintype.card (PeriodicSimplex4 N)
1163 edgeVerts := canonicalEdgeVerts4 N
1164 simplexVerts := canonicalSimplexVerts4 N
1165
1166/-- Vertex count of the canonical carrier: `N ^ 4`. -/
1167theorem canonicalCarrier4D_nV (N : ℕ) [NeZero N] :
1168 (canonicalCarrier4D N).nV = N ^ 4 :=
1169 card_vertex4 N
1170
1171/-- Edge count of the canonical carrier: `15 * N ^ 4`. -/
1172theorem canonicalCarrier4D_nE (N : ℕ) [NeZero N] :
1173 (canonicalCarrier4D N).nE = 15 * N ^ 4 :=
1174 card_periodicEdge4 N
1175
1176/-- 4-simplex count of the canonical carrier: `24 * N ^ 4`. -/
1177theorem canonicalCarrier4D_nS (N : ℕ) [NeZero N] :
1178 (canonicalCarrier4D N).nS = 24 * N ^ 4 :=
1179 card_periodicSimplex4 N
1180
1181theorem canonicalCarrier4D_no_loops (N : ℕ) [NeZero N] (hN : 2 < N) :
1182 ∀ e : Fin (canonicalCarrier4D N).nE,
1183 ((canonicalCarrier4D N).edgeVerts e).1 ≠
1184 ((canonicalCarrier4D N).edgeVerts e).2 := by
1185 intro e heq
1186 have hne := PeriodicEdge4.endpoints_ne hN (edgeFinEquiv4 N e)
1187 apply hne
1188 change (canonicalEdgeVerts4 N e).1 = (canonicalEdgeVerts4 N e).2 at heq
1189 dsimp [canonicalEdgeVerts4] at heq
1190 exact (vertexFinEquiv4 N).symm.injective heq
1191
1192theorem endpoints_injective4 (N : ℕ) [NeZero N] (hN : 1 < N)
1193 {e₁ e₂ : PeriodicEdge4 N} (h : e₁.endpoints = e₂.endpoints) :
1194 e₁ = e₂ := by
1195 rcases e₁ with ⟨b₁, d₁⟩
1196 rcases e₂ with ⟨b₂, d₂⟩
1197 have hb : b₁ = b₂ := congrArg Prod.fst h
1198 subst hb
1199 have htip :
1200 addBits4 b₁ (dispBits4 d₁).1 (dispBits4 d₁).2.1 (dispBits4 d₁).2.2.1
1201 (dispBits4 d₁).2.2.2 =
1202 addBits4 b₁ (dispBits4 d₂).1 (dispBits4 d₂).2.1 (dispBits4 d₂).2.2.1
1203 (dispBits4 d₂).2.2.2 := by
1204 simpa [PeriodicEdge4.endpoints] using congrArg Prod.snd h
1205 have hbits := addBits4_cancel_offsets N hN b₁
1206 (dispBits4 d₁).1 (dispBits4 d₁).2.1 (dispBits4 d₁).2.2.1 (dispBits4 d₁).2.2.2
1207 (dispBits4 d₂).1 (dispBits4 d₂).2.1 (dispBits4 d₂).2.2.1 (dispBits4 d₂).2.2.2
1208 htip
1209 have hd : d₁ = d₂ :=
1210 dispBits4_injective
1211 (Prod.ext hbits.1 (Prod.ext hbits.2.1 (Prod.ext hbits.2.2.1 hbits.2.2.2)))
1212 cases hd
1213 rfl
1214
1215theorem reverse_impossible4 (N : ℕ) [NeZero N] (hN : 2 < N)
1216 (e₁ e₂ : PeriodicEdge4 N) (h : e₁.endpoints = e₂.endpoints.swap) :
1217 False := by
1218 rcases e₁ with ⟨b, d⟩
1219 rcases e₂ with ⟨b', d'⟩
1220 simp only [PeriodicEdge4.endpoints, Prod.swap_prod_mk] at h
1221 obtain ⟨hb, ht⟩ := Prod.mk.inj h
1222 have hloop :
1223 addBits4 (addBits4 b' (dispBits4 d').1 (dispBits4 d').2.1
1224 (dispBits4 d').2.2.1 (dispBits4 d').2.2.2)
1225 (dispBits4 d).1 (dispBits4 d).2.1 (dispBits4 d).2.2.1
1226 (dispBits4 d).2.2.2 = b' := by
1227 rw [← hb]
1228 exact ht
1229 have hx := two_bit_steps_ne_id N hN b'.1 (dispBits4 d').1 (dispBits4 d).1
1230 (congrArg Prod.fst hloop)
1231 have hy := two_bit_steps_ne_id N hN b'.2.1 (dispBits4 d').2.1 (dispBits4 d).2.1
1232 (congrArg (fun v : Vertex4 N => v.2.1) hloop)
1233 have hz := two_bit_steps_ne_id N hN b'.2.2.1 (dispBits4 d').2.2.1
1234 (dispBits4 d).2.2.1 (congrArg (fun v : Vertex4 N => v.2.2.1) hloop)
1235 have hw := two_bit_steps_ne_id N hN b'.2.2.2 (dispBits4 d').2.2.2
1236 (dispBits4 d).2.2.2 (congrArg (fun v : Vertex4 N => v.2.2.2) hloop)
1237 exact dispBits4_ne_zero d'
1238 (Prod.ext hx.1 (Prod.ext hy.1 (Prod.ext hz.1 hw.1)))
1239
1240theorem canonicalCarrier4D_no_multiedges (N : ℕ) [NeZero N] (hN : 2 < N) :
1241 ∀ e e' : Fin (canonicalCarrier4D N).nE,
1242 sameUnorderedPair4 ((canonicalCarrier4D N).edgeVerts e)
1243 ((canonicalCarrier4D N).edgeVerts e') → e = e' := by
1244 intro e e' hpair
1245 set Eeq := edgeFinEquiv4 N
1246 set Veq := vertexFinEquiv4 N
1247 change sameUnorderedPair4 (canonicalEdgeVerts4 N e) (canonicalEdgeVerts4 N e')
1248 at hpair
1249 cases hpair with
1250 | inl hsame =>
1251 have hends : (Eeq e).endpoints = (Eeq e').endpoints := by
1252 refine Prod.ext ?_ ?_
1253 · have := congrArg (fun p => Veq p.1) hsame
1254 simpa [canonicalEdgeVerts4, Equiv.apply_symm_apply] using this
1255 · have := congrArg (fun p => Veq p.2) hsame
1256 simpa [canonicalEdgeVerts4, Equiv.apply_symm_apply] using this
1257 exact Eeq.injective
1258 (endpoints_injective4 N (lt_trans (by decide : 1 < 2) hN) hends)
1259 | inr hswap =>
1260 have hends : (Eeq e).endpoints = (Eeq e').endpoints.swap := by
1261 refine Prod.ext ?_ ?_
1262 · have := congrArg (fun p => Veq p.1) hswap
1263 simpa [canonicalEdgeVerts4, Equiv.apply_symm_apply, Prod.swap_prod_mk]
1264 using this
1265 · have := congrArg (fun p => Veq p.2) hswap
1266 simpa [canonicalEdgeVerts4, Equiv.apply_symm_apply, Prod.swap_prod_mk]
1267 using this
1268 exact (reverse_impossible4 N hN _ _ hends).elim
1269
1270theorem canonicalCarrier4D_simplex_injective (N : ℕ) [NeZero N] (hN : 2 < N) :
1271 ∀ s : Fin (canonicalCarrier4D N).nS,
1272 Function.Injective ((canonicalCarrier4D N).simplexVerts s) := by
1273 intro s a b hab
1274 set cellS := simplexFinEquiv4 N s
1275 change canonicalSimplexVerts4 N s a = canonicalSimplexVerts4 N s b at hab
1276 have hadd :
1277 addVertexBits4 cellS.1 (kuhnVerts cellS.2 a) =
1278 addVertexBits4 cellS.1 (kuhnVerts cellS.2 b) := by
1279 have := congrArg (vertexFinEquiv4 N) hab
1280 simpa [canonicalSimplexVerts4, Equiv.apply_symm_apply] using this
1281 exact kuhn_corners_injective N (lt_trans (by decide : 1 < 2) hN) cellS.1
1282 cellS.2 hadd
1283
1284theorem canonicalCarrier4D_skeleton (N : ℕ) [NeZero N]
1285 (s : Fin (canonicalCarrier4D N).nS) (i j : Fin 5) (hij : i ≠ j) :
1286 ∃ e : Fin (canonicalCarrier4D N).nE,
1287 sameUnorderedPair4 ((canonicalCarrier4D N).edgeVerts e)
1288 ((canonicalCarrier4D N).simplexVerts s i,
1289 (canonicalCarrier4D N).simplexVerts s j) := by
1290 set cellS := simplexFinEquiv4 N s
1291 let slot := pairSlot4 i j
1292 refine ⟨(edgeFinEquiv4 N).symm (localEdgeOf4 cellS.1 cellS.2 slot), ?_⟩
1293 have hInc := localEdgeOf4_endpoints_match_kuhnVerts cellS.1 cellS.2 slot
1294 change sameUnorderedPair4
1295 (canonicalEdgeVerts4 N ((edgeFinEquiv4 N).symm (localEdgeOf4 cellS.1 cellS.2 slot)))
1296 (canonicalSimplexVerts4 N s i, canonicalSimplexVerts4 N s j)
1297 simp only [canonicalEdgeVerts4, canonicalSimplexVerts4, Equiv.apply_symm_apply,
1298 sameUnorderedPair4]
1299 rcases pairSlot4_spec i j hij with hp | hp
1300 · rw [show slot = pairSlot4 i j from rfl, hp] at hInc
1301 rcases hInc with ⟨h1, h2⟩ | ⟨h1, h2⟩
1302 · left
1303 exact Prod.ext (congrArg (vertexFinEquiv4 N).symm h1.symm)
1304 (congrArg (vertexFinEquiv4 N).symm h2.symm)
1305 · right
1306 exact Prod.ext (congrArg (vertexFinEquiv4 N).symm h2.symm)
1307 (congrArg (vertexFinEquiv4 N).symm h1.symm)
1308 · rw [show slot = pairSlot4 i j from rfl, hp] at hInc
1309 rcases hInc with ⟨h1, h2⟩ | ⟨h1, h2⟩
1310 · right
1311 exact Prod.ext (congrArg (vertexFinEquiv4 N).symm h1.symm)
1312 (congrArg (vertexFinEquiv4 N).symm h2.symm)
1313 · left
1314 exact Prod.ext (congrArg (vertexFinEquiv4 N).symm h2.symm)
1315 (congrArg (vertexFinEquiv4 N).symm h1.symm)
1316
1317/-- **Headline (carrier simpliciality).** The canonical periodic Freudenthal
13184-torus carrier at side `2 < N` is simplicial: distinct edge endpoints, no
1319multi-edges, five distinct corners per Kuhn 4-simplex, and skeleton
1320closure. -/
1321theorem canonicalCarrier4D_isSimplicial (N : ℕ) [NeZero N] (hN : 2 < N) :
1322 IsSimplicial4D (canonicalCarrier4D N) :=
1323 ⟨canonicalCarrier4D_no_loops N hN, canonicalCarrier4D_no_multiedges N hN,
1324 canonicalCarrier4D_simplex_injective N hN,
1325 fun s i j hij => canonicalCarrier4D_skeleton N s i j hij⟩
1326
1327/-! ## §10. Class squared lengths and the mesh scale -/
1328
1329/-- Hamming weight of a displacement class (the squared lattice length of
1330its 0/1 displacement). -/
1331def dispWeight4 : Fin 15 → ℕ
1332 | 0 => 1
1333 | 1 => 1
1334 | 2 => 2
1335 | 3 => 1
1336 | 4 => 2
1337 | 5 => 2
1338 | 6 => 3
1339 | 7 => 1
1340 | 8 => 2
1341 | 9 => 2
1342 | 10 => 3
1343 | 11 => 2
1344 | 12 => 3
1345 | 13 => 3
1346 | 14 => 4
1347
1348/-- Squared lattice displacement determined only by the class (the 4D mirror
1349of the 3D `periodicDispSqEdge`). -/
1350def periodicDispSqEdge4 (d : Fin 15) : ℝ :=
1351 dispWeight4 d
1352
1353theorem dispWeight4_le_four (d : Fin 15) : dispWeight4 d ≤ 4 := by
1354 fin_cases d <;> decide
1355
1356theorem periodicDispSqEdge4_le_four (d : Fin 15) :
1357 periodicDispSqEdge4 d ≤ (4 : ℝ) := by
1358 unfold periodicDispSqEdge4
1359 exact_mod_cast dispWeight4_le_four d
1360
1361/-- Mesh scale at side `N`: the length of the largest class edge at lattice
1362spacing `1 / N`, which is the weight-4 hyperbody diagonal (class 14).
1363Mirrors the 3D `meshVal = sqrt 3 * spacing` (max weight 3 there). -/
1364def meshVal4D (N : ℕ) : ℝ :=
1365 Real.sqrt 4 * (N : ℝ)⁻¹
1366
1367theorem meshVal4D_pos (N : ℕ) (hN : 0 < N) : 0 < meshVal4D N :=
1368 mul_pos (Real.sqrt_pos.mpr (by norm_num)) (inv_pos.mpr (Nat.cast_pos.mpr hN))
1369
1370/-- **Mesh attainment.** The constant weight-4 class assignment (class 14,
1371the hyperbody diagonal) realizes the mesh scale on any edge, at lattice
1372spacing `1 / N`. -/
1373theorem meshVal4D_attained (N : ℕ) [NeZero N] :
1374 ∃ c : PeriodicEdge4 N → Fin 15, ∃ e : PeriodicEdge4 N,
1375 Real.sqrt ((N : ℝ)⁻¹ ^ 2 * periodicDispSqEdge4 (c e)) = meshVal4D N := by
1376 refine ⟨fun _ => 14, ⟨(0, 0, 0, 0), 0⟩, ?_⟩
1377 change Real.sqrt ((N : ℝ)⁻¹ ^ 2 * periodicDispSqEdge4 (14 : Fin 15)) = meshVal4D N
1378 have hN : (0 : ℝ) < (N : ℝ) := Nat.cast_pos.mpr (Nat.pos_of_neZero N)
1379 have hNN : (0 : ℝ) ≤ (N : ℝ)⁻¹ := le_of_lt (inv_pos.mpr hN)
1380 have h14 : periodicDispSqEdge4 (14 : Fin 15) = 4 := by
1381 unfold periodicDispSqEdge4
1382 norm_num [dispWeight4]
1383 unfold meshVal4D
1384 rw [h14, Real.sqrt_mul (sq_nonneg _), Real.sqrt_sq hNN, mul_comm]
1385
1386#print axioms canonicalCarrier4D_isSimplicial
1387#print axioms card_periodicEdge4
1388#print axioms card_periodicSimplex4
1389#print axioms displacement_classes_are_fifteen
1390#print axioms localEdgeOf4_endpoints_match_kuhnVerts
1391#print axioms kuhn_corners_injective
1392#print axioms kuhn_simplex_count_per_cube
1393#print axioms meshVal4D_attained
1394#print axioms vertexFinEquiv4
1395#print axioms edgeFinEquiv4
1396#print axioms simplexFinEquiv4
1397
1398end
1399
1400end PeriodicFreudenthalTorus4D
1401end Geometry
1402end IndisputableMonolith
1403