IndisputableMonolith.Gravity.SevenGaps.PathSumProbes
IndisputableMonolith/Gravity/SevenGaps/PathSumProbes.lean · 589 lines · 50 declarations
show as:
view math explainer →
1import IndisputableMonolith.Gravity.SevenGaps.PathSumMeasure
2import IndisputableMonolith.Geometry.PeriodicFreudenthalTorus
3
4/-!
5# Seven Gaps, Phase 2b lane O: path-sum probes C3 and C6
6
7## Status: PROBES ONLY (provenance record + landmine check).
8
9This module is NON-flag-bearing. It makes NO claim about measures, limits,
10continuum behavior, or the value of any path sum. It records two cheap
11honest facts connecting the canonical periodic Freudenthal torus
12(`Geometry.PeriodicFreudenthalTorus`) to the scoped path-sum state space
13(`PathSumMeasure.BoundedComplex`):
14
15**PROBE C3 (diagonal embedding; provenance framing ONLY).**
16`freudenthalBoundedComplex N` packages the canonical periodic Freudenthal
17torus at side `N` (any `N ≥ 1`, via `[NeZero N]`) as an element of
18`BoundedComplex (7 * N ^ 3)`. This ATTACHES the torus to the path-sum
19state space and claims nothing about measures or limits.
20* PRESERVED: the vertex/edge/tet counts (`nV = N ^ 3`, `nE = 7 * N ^ 3`,
21 `nT = 6 * N ^ 3`, proved), the edge-endpoint incidence map `edgeVerts`,
22 and the tetrahedron-corner incidence map `tetVerts`, all definitionally
23 equal to the corresponding fields of `canonicalPeriodicTriangulation N N N`
24 (`freudenthalBoundedComplex_matches_canonical`).
25* DROPPED (incidence-shape mismatch, recorded honestly): `BoundedComplex`
26 carries no `edgeInTet` field, so the edge-slot-in-tetrahedron assignment
27 of `Triangulation3D` is lost; it carries no per-tetrahedron metric field,
28 so the `tet` squared-edge geometry is lost (the scoped class is
29 equilateral-at-fixed-scale by MODEL convention); neither shape carries a
30 2-face (triangle) list. Simpliciality of the image
31 (`IsSimplicial (freudenthalBoundedComplex N)`) is NOT proved here and is
32 not claimed.
33
34**PROBE C6 (Aut vacuity landmine check). Outcome: branch (a), the
35translations EMBED.**
36The translation group `Z_N^3` (the additive group `Vertex N N N`
37`= Fin N × Fin N × Fin N` under componentwise mod-`N` addition) embeds into
38the relabeling automorphisms of the torus image:
39`translationAut N : Vertex N N N → Aut (freudenthalBoundedComplex N)` is
40injective (`translationAut_injective`), sends `0` to the identity
41relabeling (`translationAut_zero`), and sends sums to composites
42(`translationAut_add`). Consequences (each proved below):
43* `autCard_ge_translations` : `N ^ 3 ≤ |Aut(T_N)|`;
44* `mu_freudenthal_le_inv_cube` : `μ(T_N) ≤ 1 / N ^ 3`;
45* `unnormalized_torus_weight_suppressed` : the μ-weighted unitary torus
46 summand has modulus `≤ 1 / N ^ 3` for ANY action.
47
48LANDMINE RECORD (panel-mandated): because the translations embed, every
49future-wave claim of the form "the unnormalized contribution
50`μ(T_N) · exp(i·S(T_N))` is nonvanishing / dominant" MUST be rejected as
51potentially `0 = 0` unless it explicitly accounts for the
52`1/|Aut| ≤ N⁻³` suppression. The boolean outcome is recorded either way in
53`pathSumProbesStatus` (`translations_embed := true`,
54`unnormalized_mu_torus_claims_admissible := false`, both rfl-forced).
55
56## Proof notes (honesty disclosure)
57* Zero `sorry`, zero `admit`, zero new axioms, zero `native_decide`.
58* `decide` is used EXACTLY ONCE, for the concrete finite inequality
59 `(1, 0, 0) ≠ 0` in `Fin 3 × Fin 3 × Fin 3` (the nontriviality witness at
60 the concrete side `N = 3`, `nontrivial_aut_three`). Everything else is
61 symbolic (general `N` with `[NeZero N]`).
62* No `True` shells; all status flags are rfl-forced.
63-/
64
65namespace IndisputableMonolith
66namespace Gravity
67namespace SevenGaps
68namespace PathSumProbes
69
70open PathSumMeasure
71open Geometry.PeriodicFreudenthalTorus
72
73/-! ## §1. Cardinalities of the canonical periodic torus index types -/
74
75/-- The periodic vertex set at side `N` has `N ^ 3` elements. -/
76theorem card_vertex (N : ℕ) : Fintype.card (Vertex N N N) = N ^ 3 := by
77 have h : Fintype.card (Fin N × Fin N × Fin N) = N ^ 3 := by
78 rw [Fintype.card_prod, Fintype.card_prod, Fintype.card_fin]
79 ring
80 exact h
81
82/-- A positive-displacement periodic edge is exactly a (base vertex,
83displacement class) pair. -/
84def periodicEdgeEquivProd (Nx Ny Nz : ℕ) [NeZero Nx] [NeZero Ny] [NeZero Nz] :
85 PeriodicEdge Nx Ny Nz ≃ Vertex Nx Ny Nz × Fin 7 where
86 toFun e := (e.base, e.disp)
87 invFun p := ⟨p.1, p.2⟩
88 left_inv _ := rfl
89 right_inv _ := rfl
90
91/-- The periodic edge set at side `N` has `7 * N ^ 3` elements. -/
92theorem card_periodicEdge (N : ℕ) [NeZero N] :
93 Fintype.card (PeriodicEdge N N N) = 7 * N ^ 3 := by
94 rw [Fintype.card_congr (periodicEdgeEquivProd N N N), Fintype.card_prod,
95 card_vertex, Fintype.card_fin]
96 ring
97
98/-- The periodic tetrahedron set at side `N` has `6 * N ^ 3` elements. -/
99theorem card_periodicTet (N : ℕ) : Fintype.card (PeriodicTet N N N) = 6 * N ^ 3 := by
100 have h : Fintype.card (Vertex N N N × Fin 6) = 6 * N ^ 3 := by
101 rw [Fintype.card_prod, card_vertex, Fintype.card_fin]
102 ring
103 exact h
104
105/-! ## §2. PROBE C3: the torus as an element of the path-sum state space
106
107Provenance framing ONLY: this attaches the canonical torus to the scoped
108configuration class `BoundedComplex (7 * N ^ 3)`; it claims nothing about
109measures or limits. See the module docstring for the exact preserved /
110dropped data. -/
111
112/-- **PROBE C3.** The canonical periodic Freudenthal torus at side `N` as
113an element of the path-sum state space at cap `B = 7 * N ^ 3`. Counts and
114both incidence maps are inherited verbatim from
115`canonicalPeriodicTriangulation N N N`; the `edgeInTet` slot assignment and
116the per-tet metric are dropped (shape mismatch, recorded in the module
117docstring and `pathSumProbesStatus`). -/
118noncomputable def freudenthalBoundedComplex (N : ℕ) [NeZero N] :
119 BoundedComplex (7 * N ^ 3) where
120 nV := Fintype.card (Vertex N N N)
121 nE := Fintype.card (PeriodicEdge N N N)
122 nT := Fintype.card (PeriodicTet N N N)
123 hV := by
124 rw [card_vertex]
125 calc N ^ 3 = 1 * N ^ 3 := (one_mul _).symm
126 _ ≤ 7 * N ^ 3 := Nat.mul_le_mul (by norm_num) (le_refl _)
127 hE := le_of_eq (card_periodicEdge N)
128 hT := by
129 rw [card_periodicTet]
130 exact Nat.mul_le_mul (by norm_num) (le_refl _)
131 edgeVerts := canonicalEdgeVerts N N N
132 tetVerts := canonicalTetVerts N N N
133
134/-- Vertex count of the embedded torus: `N ^ 3`. -/
135theorem freudenthalBoundedComplex_nV (N : ℕ) [NeZero N] :
136 (freudenthalBoundedComplex N).nV = N ^ 3 := card_vertex N
137
138/-- Edge count of the embedded torus: `7 * N ^ 3` (the cap is met exactly). -/
139theorem freudenthalBoundedComplex_nE (N : ℕ) [NeZero N] :
140 (freudenthalBoundedComplex N).nE = 7 * N ^ 3 := card_periodicEdge N
141
142/-- Tetrahedron count of the embedded torus: `6 * N ^ 3`. -/
143theorem freudenthalBoundedComplex_nT (N : ℕ) [NeZero N] :
144 (freudenthalBoundedComplex N).nT = 6 * N ^ 3 := card_periodicTet N
145
146/-- The embedded torus is not the empty configuration: it has tetrahedra. -/
147theorem freudenthalBoundedComplex_nT_pos (N : ℕ) [NeZero N] :
148 0 < (freudenthalBoundedComplex N).nT := by
149 rw [freudenthalBoundedComplex_nT]
150 have hN : 0 < N := Nat.pos_of_neZero N
151 have h3 : 0 < N ^ 3 := pow_pos hN 3
152 omega
153
154/-- Edge-endpoint incidence is inherited verbatim from the canonical
155encoder. -/
156theorem freudenthalBoundedComplex_edgeVerts (N : ℕ) [NeZero N] :
157 (freudenthalBoundedComplex N).edgeVerts = canonicalEdgeVerts N N N := rfl
158
159/-- Tetrahedron-corner incidence is inherited verbatim from the canonical
160encoder. -/
161theorem freudenthalBoundedComplex_tetVerts (N : ℕ) [NeZero N] :
162 (freudenthalBoundedComplex N).tetVerts = canonicalTetVerts N N N := rfl
163
164/-- **PROBE C3 provenance record.** All five fields shared by the two
165incidence shapes (`nV`, `nE`, `nT`, `edgeVerts`, `tetVerts`) agree
166definitionally with `canonicalPeriodicTriangulation N N N`. What is NOT
167carried over (because `BoundedComplex` has no such fields) is the
168`edgeInTet` slot map and the per-tet metric; see the module docstring. -/
169theorem freudenthalBoundedComplex_matches_canonical (N : ℕ) [NeZero N] :
170 (freudenthalBoundedComplex N).nV =
171 (canonicalPeriodicTriangulation N N N).nV ∧
172 (freudenthalBoundedComplex N).nE =
173 (canonicalPeriodicTriangulation N N N).nE ∧
174 (freudenthalBoundedComplex N).nT =
175 (canonicalPeriodicTriangulation N N N).nT ∧
176 (freudenthalBoundedComplex N).edgeVerts =
177 (canonicalPeriodicTriangulation N N N).edgeVerts ∧
178 (freudenthalBoundedComplex N).tetVerts =
179 (canonicalPeriodicTriangulation N N N).tetVerts :=
180 ⟨rfl, rfl, rfl, rfl, rfl⟩
181
182/-! ## §3. Translation machinery
183
184The additive group `Vertex N N N = Fin N × Fin N × Fin N` (componentwise
185`Fin` addition mod `N`) acts on vertices, positive-displacement edges, and
186tetrahedra by translating the base point and fixing the displacement /
187local-tet data. The key arithmetic fact is that translation commutes with
188the `addBit`/`addBits`/`addVertexBits` offset maps of the Freudenthal
189encoding. -/
190
191/-- Translation by `t` on periodic vertices. -/
192def translateVertex {N : ℕ} [NeZero N] (t : Vertex N N N) :
193 Vertex N N N ≃ Vertex N N N where
194 toFun v := v + t
195 invFun v := v - t
196 left_inv v := by
197 show v + t - t = v
198 rw [add_sub_assoc, sub_self, add_zero]
199 right_inv v := by
200 show v - t + t = v
201 rw [sub_eq_add_neg, add_assoc, neg_add_cancel, add_zero]
202
203@[simp] theorem translateVertex_apply {N : ℕ} [NeZero N] (t v : Vertex N N N) :
204 translateVertex t v = v + t := rfl
205
206/-- Translation by `t` on positive-displacement periodic edges (translate
207the base, keep the displacement class). -/
208def translateEdge {N : ℕ} [NeZero N] (t : Vertex N N N) :
209 PeriodicEdge N N N ≃ PeriodicEdge N N N :=
210 (periodicEdgeEquivProd N N N).trans
211 ((Equiv.prodCongr (translateVertex t) (Equiv.refl (Fin 7))).trans
212 (periodicEdgeEquivProd N N N).symm)
213
214@[simp] theorem translateEdge_apply {N : ℕ} [NeZero N] (t : Vertex N N N)
215 (e : PeriodicEdge N N N) :
216 translateEdge t e = ⟨e.base + t, e.disp⟩ := rfl
217
218/-- Translation by `t` on periodic tetrahedra (translate the cell, keep the
219local Freudenthal tet index). -/
220def translateTet {N : ℕ} [NeZero N] (t : Vertex N N N) :
221 PeriodicTet N N N ≃ PeriodicTet N N N :=
222 Equiv.prodCongr (translateVertex t) (Equiv.refl (Fin 6))
223
224@[simp] theorem translateTet_apply {N : ℕ} [NeZero N] (t : Vertex N N N)
225 (p : PeriodicTet N N N) :
226 translateTet t p = (p.1 + t, p.2) := rfl
227
228/-- `addBit` commutes with translation on a `Fin N` coordinate. -/
229theorem addBit_add_right {N : ℕ} [NeZero N] (i s : Fin N) (b : Bool) :
230 addBit (i + s) b = addBit i b + s := by
231 ext
232 simp only [Geometry.PeriodicFreudenthalTorus.addBit, Fin.add_def,
233 Nat.mod_add_mod]
234 rw [add_right_comm]
235
236/-- `addBits` commutes with translation on periodic vertices. -/
237theorem addBits_add_right {N : ℕ} [NeZero N] (v t : Vertex N N N)
238 (dx dy dz : Bool) :
239 addBits (v + t) dx dy dz = addBits v dx dy dz + t := by
240 have h1 : (v + t).1 = v.1 + t.1 := rfl
241 have h2 : (v + t).2.1 = v.2.1 + t.2.1 := rfl
242 have h3 : (v + t).2.2 = v.2.2 + t.2.2 := rfl
243 unfold Geometry.PeriodicFreudenthalTorus.addBits
244 rw [h1, h2, h3, addBit_add_right, addBit_add_right, addBit_add_right]
245 rfl
246
247/-- `addVertexBits` (the local cube-corner offset) commutes with
248translation. -/
249theorem addVertexBits_add_right {N : ℕ} [NeZero N] (v t : Vertex N N N)
250 (a : Fin 8) :
251 addVertexBits (v + t) a = addVertexBits v a + t := by
252 unfold Geometry.PeriodicFreudenthalTorus.addVertexBits
253 exact addBits_add_right v t _ _ _
254
255/-- Translating an edge translates both endpoints. -/
256theorem translateEdge_endpoints {N : ℕ} [NeZero N] (t : Vertex N N N)
257 (e : PeriodicEdge N N N) :
258 (translateEdge t e).endpoints = (e.endpoints.1 + t, e.endpoints.2 + t) := by
259 show (e.base + t,
260 addBits (e.base + t) (dispBits e.disp).1 (dispBits e.disp).2.1
261 (dispBits e.disp).2.2) =
262 (e.base + t,
263 addBits e.base (dispBits e.disp).1 (dispBits e.disp).2.1
264 (dispBits e.disp).2.2 + t)
265 rw [addBits_add_right]
266
267/-- Translation by `0` is the identity on vertices. -/
268theorem translateVertex_zero {N : ℕ} [NeZero N] :
269 translateVertex (0 : Vertex N N N) = Equiv.refl _ := by
270 apply Equiv.ext
271 intro v
272 show v + 0 = v
273 rw [add_zero]
274
275/-- Translation by `0` is the identity on edges. -/
276theorem translateEdge_zero {N : ℕ} [NeZero N] :
277 translateEdge (0 : Vertex N N N) = Equiv.refl _ := by
278 apply Equiv.ext
279 intro e
280 show (⟨e.base + 0, e.disp⟩ : PeriodicEdge N N N) = e
281 rw [add_zero]
282
283/-- Translation by `0` is the identity on tetrahedra. -/
284theorem translateTet_zero {N : ℕ} [NeZero N] :
285 translateTet (0 : Vertex N N N) = Equiv.refl _ := by
286 apply Equiv.ext
287 intro p
288 show (p.1 + 0, p.2) = p
289 rw [add_zero]
290
291/-- Translations compose on vertices. -/
292theorem translateVertex_trans {N : ℕ} [NeZero N] (t s : Vertex N N N) :
293 (translateVertex t).trans (translateVertex s) = translateVertex (t + s) := by
294 apply Equiv.ext
295 intro v
296 show v + t + s = v + (t + s)
297 rw [add_assoc]
298
299/-- Translations compose on edges. -/
300theorem translateEdge_trans {N : ℕ} [NeZero N] (t s : Vertex N N N) :
301 (translateEdge t).trans (translateEdge s) = translateEdge (t + s) := by
302 apply Equiv.ext
303 intro e
304 show (⟨e.base + t + s, e.disp⟩ : PeriodicEdge N N N) = ⟨e.base + (t + s), e.disp⟩
305 rw [add_assoc]
306
307/-- Translations compose on tetrahedra. -/
308theorem translateTet_trans {N : ℕ} [NeZero N] (t s : Vertex N N N) :
309 (translateTet t).trans (translateTet s) = translateTet (t + s) := by
310 apply Equiv.ext
311 intro p
312 show (p.1 + t + s, p.2) = (p.1 + (t + s), p.2)
313 rw [add_assoc]
314
315/-! ### Conjugation through an indexing equivalence -/
316
317/-- Conjugating the identity through an indexing equivalence gives the
318identity. -/
319theorem conj_refl {α β : Type*} (E : α ≃ β) :
320 E.trans ((Equiv.refl β).trans E.symm) = Equiv.refl α := by
321 apply Equiv.ext
322 intro x
323 show E.symm (E x) = x
324 rw [Equiv.symm_apply_apply]
325
326/-- Conjugation through an indexing equivalence preserves composition. -/
327theorem conj_trans {α β : Type*} (E : α ≃ β) (σ τ : β ≃ β) :
328 (E.trans (σ.trans E.symm)).trans (E.trans (τ.trans E.symm)) =
329 E.trans ((σ.trans τ).trans E.symm) := by
330 apply Equiv.ext
331 intro x
332 show E.symm (τ (E (E.symm (σ (E x))))) = E.symm (τ (σ (E x)))
333 rw [Equiv.apply_symm_apply]
334
335/-! ## §4. PROBE C6: translations embed into the relabeling automorphisms -/
336
337/-- **PROBE C6, branch (a).** Translation by `t ∈ Z_N^3` as a relabeling
338automorphism of the embedded torus: conjugate the typed translation through
339the canonical `Fin`-indexings. Both commutation fields are proved from the
340`addBits`-translation compatibility; no finite enumeration is used. -/
341noncomputable def translationAut (N : ℕ) [NeZero N] (t : Vertex N N N) :
342 Aut (freudenthalBoundedComplex N) where
343 vEquiv := (vertexFinEquiv N N N).trans
344 ((translateVertex t).trans (vertexFinEquiv N N N).symm)
345 eEquiv := (edgeFinEquiv N N N).trans
346 ((translateEdge t).trans (edgeFinEquiv N N N).symm)
347 tEquiv := (tetFinEquiv N N N).trans
348 ((translateTet t).trans (tetFinEquiv N N N).symm)
349 edge_comm := by
350 intro e
351 show ((vertexFinEquiv N N N).symm
352 ((edgeFinEquiv N N N) ((edgeFinEquiv N N N).symm
353 (translateEdge t ((edgeFinEquiv N N N) e)))).endpoints.1,
354 (vertexFinEquiv N N N).symm
355 ((edgeFinEquiv N N N) ((edgeFinEquiv N N N).symm
356 (translateEdge t ((edgeFinEquiv N N N) e)))).endpoints.2) =
357 ((vertexFinEquiv N N N).symm (translateVertex t ((vertexFinEquiv N N N)
358 ((vertexFinEquiv N N N).symm
359 ((edgeFinEquiv N N N) e).endpoints.1))),
360 (vertexFinEquiv N N N).symm (translateVertex t ((vertexFinEquiv N N N)
361 ((vertexFinEquiv N N N).symm
362 ((edgeFinEquiv N N N) e).endpoints.2))))
363 rw [Equiv.apply_symm_apply (edgeFinEquiv N N N), translateEdge_endpoints]
364 show ((vertexFinEquiv N N N).symm
365 (((edgeFinEquiv N N N) e).endpoints.1 + t),
366 (vertexFinEquiv N N N).symm
367 (((edgeFinEquiv N N N) e).endpoints.2 + t)) =
368 ((vertexFinEquiv N N N).symm (translateVertex t ((vertexFinEquiv N N N)
369 ((vertexFinEquiv N N N).symm
370 ((edgeFinEquiv N N N) e).endpoints.1))),
371 (vertexFinEquiv N N N).symm (translateVertex t ((vertexFinEquiv N N N)
372 ((vertexFinEquiv N N N).symm
373 ((edgeFinEquiv N N N) e).endpoints.2))))
374 rw [Equiv.apply_symm_apply (vertexFinEquiv N N N),
375 Equiv.apply_symm_apply (vertexFinEquiv N N N),
376 translateVertex_apply, translateVertex_apply]
377 tet_comm := by
378 intro τ i
379 show (vertexFinEquiv N N N).symm (addVertexBits
380 ((tetFinEquiv N N N) ((tetFinEquiv N N N).symm
381 (translateTet t ((tetFinEquiv N N N) τ)))).1
382 (Geometry.FreudenthalCubeTriangulation.tetVerts
383 ((tetFinEquiv N N N) ((tetFinEquiv N N N).symm
384 (translateTet t ((tetFinEquiv N N N) τ)))).2 i)) =
385 (vertexFinEquiv N N N).symm (translateVertex t ((vertexFinEquiv N N N)
386 ((vertexFinEquiv N N N).symm (addVertexBits ((tetFinEquiv N N N) τ).1
387 (Geometry.FreudenthalCubeTriangulation.tetVerts
388 ((tetFinEquiv N N N) τ).2 i)))))
389 rw [Equiv.apply_symm_apply (tetFinEquiv N N N)]
390 show (vertexFinEquiv N N N).symm
391 (addVertexBits (((tetFinEquiv N N N) τ).1 + t)
392 (Geometry.FreudenthalCubeTriangulation.tetVerts
393 ((tetFinEquiv N N N) τ).2 i)) =
394 (vertexFinEquiv N N N).symm (translateVertex t ((vertexFinEquiv N N N)
395 ((vertexFinEquiv N N N).symm (addVertexBits ((tetFinEquiv N N N) τ).1
396 (Geometry.FreudenthalCubeTriangulation.tetVerts
397 ((tetFinEquiv N N N) τ).2 i)))))
398 rw [addVertexBits_add_right, Equiv.apply_symm_apply (vertexFinEquiv N N N),
399 translateVertex_apply]
400
401/-- Projection of `translationAut` onto its vertex permutation. -/
402theorem translationAut_vEquiv (N : ℕ) [NeZero N] (t : Vertex N N N) :
403 (translationAut N t).vEquiv =
404 (vertexFinEquiv N N N).trans
405 ((translateVertex t).trans (vertexFinEquiv N N N).symm) := rfl
406
407/-- Projection of `translationAut` onto its edge permutation. -/
408theorem translationAut_eEquiv (N : ℕ) [NeZero N] (t : Vertex N N N) :
409 (translationAut N t).eEquiv =
410 (edgeFinEquiv N N N).trans
411 ((translateEdge t).trans (edgeFinEquiv N N N).symm) := rfl
412
413/-- Projection of `translationAut` onto its tet permutation. -/
414theorem translationAut_tEquiv (N : ℕ) [NeZero N] (t : Vertex N N N) :
415 (translationAut N t).tEquiv =
416 (tetFinEquiv N N N).trans
417 ((translateTet t).trans (tetFinEquiv N N N).symm) := rfl
418
419/-- `Relabel.refl` edge projection (local helper; rfl). -/
420theorem refl_eEquiv (N : ℕ) [NeZero N] :
421 (Relabel.refl (freudenthalBoundedComplex N)).eEquiv = Equiv.refl _ := rfl
422
423/-- `Relabel.refl` tet projection (local helper; rfl). -/
424theorem refl_tEquiv (N : ℕ) [NeZero N] :
425 (Relabel.refl (freudenthalBoundedComplex N)).tEquiv = Equiv.refl _ := rfl
426
427/-- The zero translation is the identity relabeling. -/
428theorem translationAut_zero (N : ℕ) [NeZero N] :
429 translationAut N (0 : Vertex N N N) =
430 Relabel.refl (freudenthalBoundedComplex N) := by
431 apply Relabel.ext
432 · rw [translationAut_vEquiv, Relabel.refl_vEquiv, translateVertex_zero,
433 conj_refl]
434 exact rfl
435 · rw [translationAut_eEquiv, refl_eEquiv, translateEdge_zero, conj_refl]
436 exact rfl
437 · rw [translationAut_tEquiv, refl_tEquiv, translateTet_zero, conj_refl]
438 exact rfl
439
440/-- **Group-hom law.** Translation by `t + s` is the composite relabeling:
441`translationAut` together with `translationAut_zero` is a monoid-hom
442package from `Z_N^3` into the automorphisms under `Relabel.trans`. -/
443theorem translationAut_add (N : ℕ) [NeZero N] (t s : Vertex N N N) :
444 translationAut N (t + s) =
445 (translationAut N t).trans (translationAut N s) := by
446 apply Relabel.ext
447 · rw [Relabel.trans_vEquiv, translationAut_vEquiv, translationAut_vEquiv,
448 translationAut_vEquiv, conj_trans, translateVertex_trans]
449 · rw [Relabel.trans_eEquiv, translationAut_eEquiv, translationAut_eEquiv,
450 translationAut_eEquiv, conj_trans, translateEdge_trans]
451 · rw [Relabel.trans_tEquiv, translationAut_tEquiv, translationAut_tEquiv,
452 translationAut_tEquiv, conj_trans, translateTet_trans]
453
454/-- **Injectivity.** Distinct translations give distinct relabelings: the
455image vertex permutation of `t` recovers `t` at the origin. -/
456theorem translationAut_injective (N : ℕ) [NeZero N] :
457 Function.Injective (translationAut N) := by
458 intro t s h
459 have hv : (translationAut N t).vEquiv ((vertexFinEquiv N N N).symm 0) =
460 (translationAut N s).vEquiv ((vertexFinEquiv N N N).symm 0) := by
461 rw [h]
462 rw [translationAut_vEquiv, translationAut_vEquiv] at hv
463 have hv' : (vertexFinEquiv N N N).symm
464 (translateVertex t ((vertexFinEquiv N N N)
465 ((vertexFinEquiv N N N).symm 0))) =
466 (vertexFinEquiv N N N).symm
467 (translateVertex s ((vertexFinEquiv N N N)
468 ((vertexFinEquiv N N N).symm 0))) := hv
469 rw [Equiv.apply_symm_apply (vertexFinEquiv N N N), translateVertex_apply,
470 translateVertex_apply] at hv'
471 have h0 : (0 : Vertex N N N) + t = 0 + s :=
472 (vertexFinEquiv N N N).symm.injective hv'
473 rw [zero_add, zero_add] at h0
474 exact h0
475
476/-- **PROBE C6 headline (branch (a) holds: translations EMBED).** The
477translation group `Z_N^3` embeds into the relabeling automorphisms of the
478embedded torus: an injective map that is a monoid hom for `Relabel.trans`. -/
479theorem translations_embed_in_aut (N : ℕ) [NeZero N] :
480 ∃ f : Vertex N N N → Aut (freudenthalBoundedComplex N),
481 Function.Injective f ∧
482 f 0 = Relabel.refl (freudenthalBoundedComplex N) ∧
483 ∀ t s, f (t + s) = (f t).trans (f s) :=
484 ⟨translationAut N, translationAut_injective N, translationAut_zero N,
485 translationAut_add N⟩
486
487/-- A nonzero translation is a nontrivial automorphism. -/
488theorem translationAut_ne_refl (N : ℕ) [NeZero N] {t : Vertex N N N}
489 (ht : t ≠ 0) :
490 translationAut N t ≠ Relabel.refl (freudenthalBoundedComplex N) := by
491 intro hEq
492 exact ht (translationAut_injective N (hEq.trans (translationAut_zero N).symm))
493
494/-- **LANDMINE, count form.** `|Aut(T_N)| ≥ N ^ 3`. -/
495theorem autCard_ge_translations (N : ℕ) [NeZero N] :
496 N ^ 3 ≤ Nat.card (Aut (freudenthalBoundedComplex N)) := by
497 have h := Nat.card_le_card_of_injective (translationAut N)
498 (translationAut_injective N)
499 rwa [Nat.card_eq_fintype_card, card_vertex] at h
500
501/-- **LANDMINE, measure form.** `μ(T_N) ≤ 1 / N ^ 3`: the symmetry factor
502suppresses the torus configuration by at least its translation-orbit size. -/
503theorem mu_freudenthal_le_inv_cube (N : ℕ) [NeZero N] :
504 mu (freudenthalBoundedComplex N) ≤ 1 / ((N : ℝ) ^ 3) := by
505 have hNpos : (0 : ℝ) < (N : ℝ) := by
506 exact_mod_cast Nat.pos_of_neZero N
507 have hN : (0 : ℝ) < (N : ℝ) ^ 3 := pow_pos hNpos 3
508 have hle : ((N : ℝ) ^ 3) ≤
509 (Nat.card (Aut (freudenthalBoundedComplex N)) : ℝ) := by
510 exact_mod_cast autCard_ge_translations N
511 unfold PathSumMeasure.mu
512 exact one_div_le_one_div_of_le hN hle
513
514/-- **LANDMINE, summand form (the panel-mandated rejection criterion).**
515For ANY real action `S`, the μ-weighted unitary summand of the embedded
516torus has modulus at most `N⁻³`. Consequence sentence: every future-wave
517claim that the unnormalized contribution `μ(T_N)·exp(i·S(T_N))` is
518nonvanishing or dominant must be rejected as potentially `0 = 0` unless it
519explicitly survives this `1/|Aut|` suppression. -/
520theorem unnormalized_torus_weight_suppressed (N : ℕ) [NeZero N]
521 (S : BoundedComplex (7 * N ^ 3) → ℝ) :
522 ‖(mu (freudenthalBoundedComplex N) : ℂ) *
523 unitaryWeight S (freudenthalBoundedComplex N)‖ ≤ 1 / ((N : ℝ) ^ 3) := by
524 rw [norm_mul, Complex.norm_real, unitaryWeight_norm, mul_one,
525 Real.norm_eq_abs, abs_of_pos (mu_pos _)]
526 exact mu_freudenthal_le_inv_cube N
527
528/-! ### Concrete instantiation at N = 3 -/
529
530/-- The embedding is injective at the concrete side `N = 3`. -/
531theorem translationAut_three_injective :
532 Function.Injective (translationAut 3) := translationAut_injective 3
533
534/-- `|Aut(T_3)| ≥ 27`. -/
535theorem autCard_ge_27 :
536 27 ≤ Nat.card (Aut (freudenthalBoundedComplex 3)) := by
537 have h := autCard_ge_translations 3
538 norm_num at h
539 exact h
540
541/-- A concrete nontrivial automorphism at `N = 3`: translation by
542`(1, 0, 0)`. (`decide` is used here, once, for the finite inequality
543`(1, 0, 0) ≠ 0` in `Fin 3 × Fin 3 × Fin 3`; no `native_decide`.) -/
544theorem nontrivial_aut_three :
545 translationAut 3 ((1, 0, 0) : Vertex 3 3 3) ≠
546 Relabel.refl (freudenthalBoundedComplex 3) :=
547 translationAut_ne_refl 3 (by decide)
548
549/-! ## §5. Status ledger (the recorded boolean outcomes; rfl-forced) -/
550
551/-- Outcome record for probes C3 and C6. No `True` shells; every flag is
552forced by `rfl` below. -/
553structure ProbeStatus where
554 torus_attached_to_state_space : Bool
555 counts_and_incidence_preserved : Bool
556 edge_in_tet_slots_preserved : Bool
557 per_tet_metric_preserved : Bool
558 simpliciality_of_image_proved : Bool
559 translations_embed : Bool
560 unnormalized_mu_torus_claims_admissible : Bool
561
562/-- The probe outcomes: C3 attached (counts + incidence preserved; edge-slot
563and metric data dropped; simpliciality of the image not claimed), C6 branch
564(a) held (translations embed), hence unnormalized `μ(T_N)·exp(iS)` claims
565are NOT admissible without addressing the `1/|Aut|` suppression. -/
566def pathSumProbesStatus : ProbeStatus where
567 torus_attached_to_state_space := true
568 counts_and_incidence_preserved := true
569 edge_in_tet_slots_preserved := false
570 per_tet_metric_preserved := false
571 simpliciality_of_image_proved := false
572 translations_embed := true
573 unnormalized_mu_torus_claims_admissible := false
574
575theorem pathSumProbesStatus_flags :
576 pathSumProbesStatus.torus_attached_to_state_space = true ∧
577 pathSumProbesStatus.counts_and_incidence_preserved = true ∧
578 pathSumProbesStatus.edge_in_tet_slots_preserved = false ∧
579 pathSumProbesStatus.per_tet_metric_preserved = false ∧
580 pathSumProbesStatus.simpliciality_of_image_proved = false ∧
581 pathSumProbesStatus.translations_embed = true ∧
582 pathSumProbesStatus.unnormalized_mu_torus_claims_admissible = false :=
583 ⟨rfl, rfl, rfl, rfl, rfl, rfl, rfl⟩
584
585end PathSumProbes
586end SevenGaps
587end Gravity
588end IndisputableMonolith
589