IndisputableMonolith.Gravity.FreudenthalAxisStencilCoeffCert
IndisputableMonolith/Gravity/FreudenthalAxisStencilCoeffCert.lean · 1582 lines · 115 declarations
show as:
view math explainer →
1import IndisputableMonolith.Gravity.PhysicalSixTetCubicDirichletInstance
2
3/-!
4# Corrected Freudenthal axis-stencil coefficient certificate
5
6This module mirrors the exact rational audit in
7`scripts/freudenthal_explicit_fiber_endpoint_analysis.py`.
8
9It does not use floating-point arithmetic. The certificate checks the
10coefficient of every unordered monomial `xi(u) * xi(v)` in the corrected
11`N = 5` mixed explicit-fiber axis-stencil residual.
12-/
13
14namespace IndisputableMonolith
15namespace Gravity
16namespace FreudenthalAxisStencilCoeffCert
17
18open Geometry.PeriodicFreudenthalTorus
19open Geometry.FreudenthalCubeTriangulation
20open Geometry.ReggeRigorousFoundation
21open PhysicalSixTetCubicDirichletInstance
22
23abbrev Vertex5 := Vertex 5 5 5
24abbrev PeriodicEdge5 := PeriodicEdge 5 5 5
25
26def addFin5 (i j : Fin 5) : Fin 5 :=
27 ⟨(i.1 + j.1) % 5, by omega⟩
28
29def negFin5 (i : Fin 5) : Fin 5 :=
30 ⟨(5 - i.1) % 5, by omega⟩
31
32theorem addFin5_zero_left (i : Fin 5) :
33 addFin5 0 i = i := by
34 ext
35 simp [addFin5]
36
37theorem addFin5_neg_self (i : Fin 5) :
38 addFin5 (negFin5 i) i = 0 := by
39 ext
40 simp [addFin5, negFin5]
41
42theorem addFin5_neg_add_self (a i : Fin 5) :
43 addFin5 (negFin5 a) (addFin5 a i) = i := by
44 ext
45 simp [addFin5, negFin5]
46 omega
47
48theorem addFin5_self_add_neg (a i : Fin 5) :
49 addFin5 a (addFin5 (negFin5 a) i) = i := by
50 ext
51 simp [addFin5, negFin5]
52 omega
53
54def translateVertex5 (a v : Vertex5) : Vertex5 :=
55 (addFin5 a.1 v.1, addFin5 a.2.1 v.2.1, addFin5 a.2.2 v.2.2)
56
57def negVertex5 (v : Vertex5) : Vertex5 :=
58 (negFin5 v.1, negFin5 v.2.1, negFin5 v.2.2)
59
60def relativeVertex5 (base v : Vertex5) : Vertex5 :=
61 translateVertex5 (negVertex5 base) v
62
63def translateEdge5 (a : Vertex5) (edge : PeriodicEdge5) : PeriodicEdge5 :=
64 { base := translateVertex5 a edge.base, disp := edge.disp }
65
66theorem translateVertex5_neg_left (a v : Vertex5) :
67 translateVertex5 (negVertex5 a) (translateVertex5 a v) = v := by
68 rcases a with ⟨ax, ay, az⟩
69 rcases v with ⟨x, y, z⟩
70 ext <;> simp [translateVertex5, negVertex5, addFin5_neg_add_self]
71
72theorem translateVertex5_neg_right (a v : Vertex5) :
73 translateVertex5 a (translateVertex5 (negVertex5 a) v) = v := by
74 rcases a with ⟨ax, ay, az⟩
75 rcases v with ⟨x, y, z⟩
76 ext <;> simp [translateVertex5, negVertex5, addFin5_self_add_neg]
77
78def translateVertex5Equiv (a : Vertex5) : Vertex5 ≃ Vertex5 where
79 toFun := translateVertex5 a
80 invFun := translateVertex5 (negVertex5 a)
81 left_inv := translateVertex5_neg_left a
82 right_inv := translateVertex5_neg_right a
83
84def translateEdge5Equiv (a : Vertex5) : PeriodicEdge5 ≃ PeriodicEdge5 where
85 toFun := translateEdge5 a
86 invFun := translateEdge5 (negVertex5 a)
87 left_inv := by
88 intro edge
89 rcases edge with ⟨base, disp⟩
90 simp [translateEdge5, translateVertex5_neg_left]
91 right_inv := by
92 intro edge
93 rcases edge with ⟨base, disp⟩
94 simp [translateEdge5, translateVertex5_neg_right]
95
96def subOneMod5 (i : Fin 5) : Fin 5 :=
97 ⟨(i.1 + 4) % 5, by omega⟩
98
99def subBit5 (i : Fin 5) (b : Bool) : Fin 5 :=
100 if b then subOneMod5 i else i
101
102theorem subBit5_addFin5 (a i : Fin 5) (b : Bool) :
103 subBit5 (addFin5 a i) b = addFin5 a (subBit5 i b) := by
104 cases b <;> ext <;> simp [subBit5, subOneMod5, addFin5]
105 omega
106
107def matchingBaseCell5 (a : Fin 8) (target : Vertex5) : Vertex5 :=
108 let b := vertexBits a
109 (subBit5 target.1 b.1, subBit5 target.2.1 b.2.1, subBit5 target.2.2 b.2.2)
110
111theorem matchingBaseCell5_spec (a : Fin 8) (target : Vertex5) :
112 target = addVertexBits (matchingBaseCell5 a target) a := by
113 rcases target with ⟨x, y, z⟩
114 fin_cases x <;> fin_cases y <;> fin_cases z <;> fin_cases a <;> decide
115
116def selectedCell5 (edge : PeriodicEdge5) (pair : FreudenthalLocalPair) : Vertex5 :=
117 matchingBaseCell5 (cubeEdgeBase (localEdgeOf pair.1 pair.2)) edge.base
118
119theorem selectedCell5_eq_freudenthalExplicitFiberPairSelectedCell
120 (edge : PeriodicEdge5) (pair : FreudenthalLocalPair) :
121 selectedCell5 edge pair =
122 freudenthalExplicitFiberPairSelectedCell edge pair := by
123 unfold selectedCell5 freudenthalExplicitFiberPairSelectedCell
124 exact periodicMatchingBaseCell_unique
125 (cubeEdgeBase (localEdgeOf pair.1 pair.2)) edge.base
126 (matchingBaseCell5_spec (cubeEdgeBase (localEdgeOf pair.1 pair.2)) edge.base)
127
128theorem matchingBaseCell5_translate (a target : Vertex5) (b : Fin 8) :
129 matchingBaseCell5 b (translateVertex5 a target) =
130 translateVertex5 a (matchingBaseCell5 b target) := by
131 rcases a with ⟨ax, ay, az⟩
132 rcases target with ⟨x, y, z⟩
133 fin_cases b <;>
134 ext <;>
135 simp [matchingBaseCell5, translateVertex5, vertexBits, subBit5_addFin5]
136
137theorem selectedCell5_translate (a : Vertex5) (edge : PeriodicEdge5)
138 (pair : FreudenthalLocalPair) :
139 selectedCell5 (translateEdge5 a edge) pair =
140 translateVertex5 a (selectedCell5 edge pair) := by
141 simp [selectedCell5, translateEdge5, matchingBaseCell5_translate]
142
143theorem addVertexBits_translate5 (a cell : Vertex5) (b : Fin 8) :
144 addVertexBits (translateVertex5 a cell) b =
145 translateVertex5 a (addVertexBits cell b) := by
146 rcases a with ⟨ax, ay, az⟩
147 rcases cell with ⟨x, y, z⟩
148 fin_cases b <;>
149 ext <;>
150 simp [addVertexBits, addBits, translateVertex5, addBit, addFin5, bit, vertexBits]
151 all_goals omega
152
153theorem translateEdge5_endpoints (a : Vertex5) (edge : PeriodicEdge5) :
154 (translateEdge5 a edge).endpoints =
155 (translateVertex5 a edge.endpoints.1, translateVertex5 a edge.endpoints.2) := by
156 rcases a with ⟨ax, ay, az⟩
157 rcases edge with ⟨base, disp⟩
158 rcases base with ⟨x, y, z⟩
159 fin_cases disp <;>
160 ext <;>
161 simp [translateEdge5, PeriodicEdge.endpoints, addBits, dispBits, translateVertex5,
162 addBit, addFin5, bit]
163 all_goals omega
164
165def sqEdgeRat : Fin 6 → Rat
166 | 0 => 1
167 | 1 => 2
168 | 2 => 3
169 | 3 => 1
170 | 4 => 2
171 | 5 => 1
172
173def snormRat : Fin 6 → Fin 6 → Rat
174 | 0, 0 => 0
175 | 0, 1 => 0
176 | 0, 2 => 0
177 | 0, 3 => 0
178 | 0, 4 => -1
179 | 0, 5 => 2
180 | 1, 0 => 0
181 | 1, 1 => 2
182 | 1, 2 => -2
183 | 1, 3 => -4
184 | 1, 4 => 4
185 | 1, 5 => -2
186 | 2, 0 => 0
187 | 2, 1 => -3
188 | 2, 2 => 2
189 | 2, 3 => 6
190 | 2, 4 => -3
191 | 2, 5 => 0
192 | 3, 0 => 0
193 | 3, 1 => -2
194 | 3, 2 => 2
195 | 3, 3 => 2
196 | 3, 4 => -2
197 | 3, 5 => 0
198 | 4, 0 => -2
199 | 4, 1 => 4
200 | 4, 2 => -2
201 | 4, 3 => -4
202 | 4, 4 => 2
203 | 4, 5 => 0
204 | 5, 0 => 2
205 | 5, 1 => -1
206 | 5, 2 => 0
207 | 5, 3 => 0
208 | 5, 4 => 0
209 | 5, 5 => 0
210
211theorem sqEdgeRat_cast_eq_freudenthalTetSqEdges (k : Fin 6) :
212 (sqEdgeRat k : ℝ) =
213 Geometry.FreudenthalCubeTriangulation.freudenthalTetSqEdges k := by
214 fin_cases k <;> norm_num [sqEdgeRat,
215 Geometry.FreudenthalCubeTriangulation.freudenthalTetSqEdges]
216
217theorem snormRat_cast_eq_freudenthalSchlaefliTable (e k : Fin 6) :
218 (snormRat e k : ℝ) =
219 FreudenthalLengthChainEndpointCert.freudenthalSchlaefliPolySummandNormTable e k := by
220 fin_cases e <;> fin_cases k <;> norm_num [snormRat,
221 FreudenthalLengthChainEndpointCert.freudenthalSchlaefliPolySummandNormTable]
222
223theorem freudenthalLocalPairDisp_eq_of_mem
224 (edge : PeriodicEdge5) (pair : FreudenthalLocalPair)
225 (hpair : pair ∈ freudenthalLocalPairDispFiber edge.disp) :
226 freudenthalLocalPairDisp pair = edge.disp := by
227 have h := hpair
228 rw [freudenthalLocalPairDispFiber_eq_filter edge.disp] at h
229 exact (Finset.mem_filter.mp h).2
230
231theorem periodicDispSqEdge_eq_freudenthalTetSqEdges_of_mem
232 (edge : PeriodicEdge5) (pair : FreudenthalLocalPair)
233 (hpair : pair ∈ freudenthalLocalPairDispFiber edge.disp) :
234 periodicDispSqEdge edge.disp =
235 Geometry.FreudenthalCubeTriangulation.freudenthalTetSqEdges pair.2 := by
236 have hdisp := freudenthalLocalPairDisp_eq_of_mem edge pair hpair
237 have hsq :=
238 freudenthalTet_sqEdge_eq_periodicDispSqEdge_localEdgeOf
239 (Nx := 5) (Ny := 5) (Nz := 5)
240 (selectedCell5 edge pair) pair.1 pair.2
241 rw [← hdisp]
242 simpa [freudenthalLocalPairDisp, Geometry.FreudenthalCubeTriangulation.freudenthalTet]
243 using hsq.symm
244
245def sameUnordered (a b u v : Vertex5) : Bool :=
246 decide ((a = u ∧ b = v) ∨ (a = v ∧ b = u))
247
248theorem sameUnordered_translate (a x y u v : Vertex5) :
249 sameUnordered (translateVertex5 a x) (translateVertex5 a y)
250 (translateVertex5 a u) (translateVertex5 a v) =
251 sameUnordered x y u v := by
252 have hinj : Function.Injective (translateVertex5 a) :=
253 (translateVertex5Equiv a).injective
254 simp [sameUnordered, hinj.eq_iff]
255
256def scaledPairLocalVertexCoeff
257 (edge : PeriodicEdge5) (pair : FreudenthalLocalPair) (k : Fin 6)
258 (endpoint : Vertex5) (u v : Vertex5) : Rat :=
259 let cell := selectedCell5 edge pair
260 let ev := edgeVertices k
261 let v0 := addVertexBits cell (tetVerts pair.1 ev.1)
262 let v1 := addVertexBits cell (tetVerts pair.1 ev.2)
263 let c := snormRat pair.2 k * sqEdgeRat k / 4
264 (if sameUnordered endpoint v0 u v then -c / 2 else 0) +
265 (if sameUnordered endpoint v1 u v then -c / 2 else 0)
266
267theorem scaledPairLocalVertexCoeff_translate
268 (a : Vertex5) (edge : PeriodicEdge5) (pair : FreudenthalLocalPair) (k : Fin 6)
269 (endpoint u v : Vertex5) :
270 scaledPairLocalVertexCoeff (translateEdge5 a edge) pair k
271 (translateVertex5 a endpoint) (translateVertex5 a u) (translateVertex5 a v) =
272 scaledPairLocalVertexCoeff edge pair k endpoint u v := by
273 simp [scaledPairLocalVertexCoeff, selectedCell5_translate, addVertexBits_translate5,
274 sameUnordered_translate]
275
276def mixedAxisEdgeLhsCoeff (edge : PeriodicEdge5) (u v : Vertex5) : Rat :=
277 let ep := edge.endpoints
278 ∑ pair ∈ freudenthalLocalPairDispFiber edge.disp,
279 ∑ k : Fin 6,
280 (scaledPairLocalVertexCoeff edge pair k ep.1 u v +
281 scaledPairLocalVertexCoeff edge pair k ep.2 u v)
282
283theorem mixedAxisEdgeLhsCoeff_translate
284 (a : Vertex5) (edge : PeriodicEdge5) (u v : Vertex5) :
285 mixedAxisEdgeLhsCoeff (translateEdge5 a edge)
286 (translateVertex5 a u) (translateVertex5 a v) =
287 mixedAxisEdgeLhsCoeff edge u v := by
288 dsimp only [mixedAxisEdgeLhsCoeff]
289 rw [show (translateEdge5 a edge).disp = edge.disp by rfl]
290 rw [translateEdge5_endpoints]
291 apply Finset.sum_congr rfl
292 intro pair hpair
293 apply Finset.sum_congr rfl
294 intro k hk
295 simp only [scaledPairLocalVertexCoeff_translate]
296
297def mixedAxisLhsCoeff (u v : Vertex5) : Rat :=
298 ∑ edge : PeriodicEdge5, mixedAxisEdgeLhsCoeff edge u v
299
300theorem mixedAxisLhsCoeff_eq_sum_edge (u v : Vertex5) :
301 mixedAxisLhsCoeff u v = ∑ edge : PeriodicEdge5, mixedAxisEdgeLhsCoeff edge u v := rfl
302
303def axisStencilResidualCoeff (u v : Vertex5) : Rat :=
304 ∑ base : Vertex5, ∑ d : Fin 3,
305 let edge : PeriodicEdge5 := { base := base, disp := periodicAxisDisp d }
306 let ep := edge.endpoints
307 (if ep.1 = u && ep.1 = v then -2 else 0) +
308 (if ep.2 = u && ep.2 = v then -2 else 0) +
309 (if sameUnordered ep.1 ep.2 u v then 4 else 0)
310
311def mixedAxisResidualCoeff (u v : Vertex5) : Rat :=
312 mixedAxisLhsCoeff u v + axisStencilResidualCoeff u v
313
314def originVertex : Vertex5 :=
315 (0, 0, 0)
316
317theorem translateVertex5_origin_left (v : Vertex5) :
318 translateVertex5 originVertex v = v := by
319 rcases v with ⟨x, y, z⟩
320 ext <;> simp [translateVertex5, originVertex, addFin5_zero_left]
321
322theorem relativeVertex5_origin_eq_self (v : Vertex5) :
323 relativeVertex5 originVertex v = v := by
324 rw [relativeVertex5]
325 rw [show negVertex5 originVertex = originVertex by
326 ext <;> simp [negVertex5, negFin5, originVertex]]
327 exact translateVertex5_origin_left v
328
329theorem relativeVertex5_self_eq_origin (v : Vertex5) :
330 relativeVertex5 v v = originVertex := by
331 rcases v with ⟨x, y, z⟩
332 ext <;> simp [relativeVertex5, translateVertex5, negVertex5, addFin5, negFin5, originVertex]
333
334/-- Full coefficient-vanishing statement for the corrected `N = 5` axis-stencil
335residual. This is the finite certificate still needed before converting the
336coefficient audit into `CanonicalPeriodicMixedHingeDeficitExplicitFiberAxisStencilTargetAtN5`. -/
337def FullResidualCoeffCert : Prop :=
338 ∀ u v : Vertex5, mixedAxisResidualCoeff u v = 0
339
340/-- Translation invariance of the mixed explicit-fiber LHS coefficient model.
341This is now the only heavy finite reindexing bridge left in the corrected
342axis-stencil coefficient certificate. -/
343def MixedAxisLhsCoeffTranslationInvariant : Prop :=
344 ∀ u v : Vertex5,
345 mixedAxisLhsCoeff u v =
346 mixedAxisLhsCoeff originVertex (relativeVertex5 u v)
347
348/-- Edge-summand form of the mixed LHS translation bridge. This is the
349remaining local target after factoring `mixedAxisLhsCoeff` as a sum over
350`PeriodicEdge5`. -/
351def MixedAxisEdgeLhsCoeffTranslationInvariant : Prop :=
352 ∀ (a : Vertex5) (edge : PeriodicEdge5) (u v : Vertex5),
353 mixedAxisEdgeLhsCoeff (translateEdge5 a edge)
354 (translateVertex5 a u) (translateVertex5 a v) =
355 mixedAxisEdgeLhsCoeff edge u v
356
357theorem mixedAxisLhsCoeff_translationInvariant_of_edge
358 (hedge : MixedAxisEdgeLhsCoeffTranslationInvariant) :
359 MixedAxisLhsCoeffTranslationInvariant := by
360 intro u v
361 let a := negVertex5 u
362 have hsum :
363 mixedAxisLhsCoeff (translateVertex5 a u) (translateVertex5 a v) =
364 mixedAxisLhsCoeff u v := by
365 unfold mixedAxisLhsCoeff
366 symm
367 exact Fintype.sum_equiv (translateEdge5Equiv a)
368 (fun edge : PeriodicEdge5 => mixedAxisEdgeLhsCoeff edge u v)
369 (fun edge : PeriodicEdge5 =>
370 mixedAxisEdgeLhsCoeff edge (translateVertex5 a u) (translateVertex5 a v))
371 (fun edge => by
372 exact (hedge a edge u v).symm)
373 have hu : translateVertex5 a u = originVertex := by
374 dsimp [a]
375 exact relativeVertex5_self_eq_origin u
376 have hv : translateVertex5 a v = relativeVertex5 u v := by
377 rfl
378 rw [hu, hv] at hsum
379 exact hsum.symm
380
381def rowMixedAxisLhsCoeffTranslationInvariant (u : Vertex5) : Bool :=
382 decide (∀ v : Vertex5,
383 mixedAxisLhsCoeff u v =
384 mixedAxisLhsCoeff originVertex (relativeVertex5 u v))
385
386/-- Translation invariance of the corrected three-axis stencil coefficient
387model. This side is small enough to certify directly in Lean. -/
388def AxisStencilResidualCoeffTranslationInvariant : Prop :=
389 ∀ u v : Vertex5,
390 axisStencilResidualCoeff u v =
391 axisStencilResidualCoeff originVertex (relativeVertex5 u v)
392
393/-- Translation-invariance bridge for the rational residual coefficient model.
394Once proved, the origin-row certificate gives the full 125-by-125 table without
395naively compiling every row. -/
396def MixedAxisResidualCoeffTranslationInvariant : Prop :=
397 ∀ u v : Vertex5,
398 mixedAxisResidualCoeff u v =
399 mixedAxisResidualCoeff originVertex (relativeVertex5 u v)
400
401def axisStencilResidualCoeffTranslationInvariantCheck : Bool :=
402 decide (∀ u v : Vertex5,
403 axisStencilResidualCoeff u v =
404 axisStencilResidualCoeff originVertex (relativeVertex5 u v))
405
406theorem axisStencilResidualCoeffTranslationInvariantCheck_eq_true :
407 axisStencilResidualCoeffTranslationInvariantCheck = true := by
408 native_decide
409
410theorem axisStencilResidualCoeff_translationInvariant :
411 AxisStencilResidualCoeffTranslationInvariant := by
412 change ∀ u v : Vertex5,
413 axisStencilResidualCoeff u v =
414 axisStencilResidualCoeff originVertex (relativeVertex5 u v)
415 exact of_decide_eq_true
416 (by
417 simpa [axisStencilResidualCoeffTranslationInvariantCheck] using
418 axisStencilResidualCoeffTranslationInvariantCheck_eq_true)
419
420theorem mixedAxisResidualCoeff_translationInvariant_of_lhs
421 (hlhs : MixedAxisLhsCoeffTranslationInvariant) :
422 MixedAxisResidualCoeffTranslationInvariant := by
423 intro u v
424 unfold mixedAxisResidualCoeff
425 rw [hlhs u v, axisStencilResidualCoeff_translationInvariant u v]
426
427/-- Translation-normalized exact rational coefficient audit for the corrected
428`N = 5` axis-stencil target. The companion Python audit checks all unordered
429vertex pairs; this Lean theorem checks the 125 origin-offset representatives in
430the same rational coefficient model. -/
431def originResidualCoeffsZero : Bool :=
432 decide (∀ v : Vertex5, mixedAxisResidualCoeff originVertex v = 0)
433
434theorem originResidualCoeffsZero_eq_true :
435 originResidualCoeffsZero = true := by
436 native_decide
437
438theorem originResidualCoeffCert :
439 ∀ v : Vertex5, mixedAxisResidualCoeff originVertex v = 0 := by
440 exact of_decide_eq_true originResidualCoeffsZero_eq_true
441
442theorem fullResidualCoeffCert_of_translationInvariant
443 (htrans : MixedAxisResidualCoeffTranslationInvariant) :
444 FullResidualCoeffCert := by
445 intro u v
446 rw [htrans u v]
447 exact originResidualCoeffCert (relativeVertex5 u v)
448
449theorem fullResidualCoeffCert_of_lhs_translationInvariant
450 (hlhs : MixedAxisLhsCoeffTranslationInvariant) :
451 FullResidualCoeffCert :=
452 fullResidualCoeffCert_of_translationInvariant
453 (mixedAxisResidualCoeff_translationInvariant_of_lhs hlhs)
454
455theorem fullResidualCoeffCert_of_edge_lhs_translationInvariant
456 (hedge : MixedAxisEdgeLhsCoeffTranslationInvariant) :
457 FullResidualCoeffCert :=
458 fullResidualCoeffCert_of_lhs_translationInvariant
459 (mixedAxisLhsCoeff_translationInvariant_of_edge hedge)
460
461theorem mixedAxisEdgeLhsCoeff_translationInvariant :
462 MixedAxisEdgeLhsCoeffTranslationInvariant := by
463 intro a edge u v
464 exact mixedAxisEdgeLhsCoeff_translate a edge u v
465
466theorem mixedAxisLhsCoeff_translationInvariant :
467 MixedAxisLhsCoeffTranslationInvariant :=
468 mixedAxisLhsCoeff_translationInvariant_of_edge mixedAxisEdgeLhsCoeff_translationInvariant
469
470theorem fullResidualCoeffCert :
471 FullResidualCoeffCert :=
472 fullResidualCoeffCert_of_edge_lhs_translationInvariant
473 mixedAxisEdgeLhsCoeff_translationInvariant
474
475/-- Canonical `N = 5` encoded periodic Freudenthal torus used by the corrected
476axis-stencil certificate. -/
477noncomputable abbrev P5 :=
478 canonicalEncodedPeriodicFreudenthalTorus 5 5 5 (by decide) (by decide) (by decide)
479
480abbrev VertexPotential5 :=
481 Geometry.ReggeHessian3D.VertexPotential P5.K
482
483noncomputable def potentialAtVertex5 (ξ : VertexPotential5) (v : Vertex5) : ℝ :=
484 ξ ((vertexFinEquiv 5 5 5).symm v)
485
486/-- The flat local edge-length derivative at the selected explicit-fiber cell,
487rewritten in the same typed vertex coordinates used by the coefficient atoms. -/
488theorem freudenthalExplicitFiberFlatLocalEdgeLengthDirectionalDeriv_selectedCell5
489 (ξ : VertexPotential5) (edge : PeriodicEdge5) (pair : FreudenthalLocalPair)
490 (k : Fin 6) :
491 freudenthalExplicitFiberFlatLocalEdgeLengthDirectionalDeriv
492 (by decide) (by decide) (by decide) ξ (selectedCell5 edge pair) pair.1 k =
493 let ev := edgeVertices k
494 let v0 := addVertexBits (selectedCell5 edge pair) (tetVerts pair.1 ev.1)
495 let v1 := addVertexBits (selectedCell5 edge pair) (tetVerts pair.1 ev.2)
496 Real.sqrt (Geometry.FreudenthalCubeTriangulation.freudenthalTetSqEdges k) *
497 ((potentialAtVertex5 ξ v0 + potentialAtVertex5 ξ v1) / 2) := by
498 rw [selectedCell5_eq_freudenthalExplicitFiberPairSelectedCell edge pair]
499 unfold freudenthalExplicitFiberFlatLocalEdgeLengthDirectionalDeriv potentialAtVertex5
500 dsimp
501 rw [freudenthalExplicitFiber_canonicalTetVerts_eq
502 (by decide) (by decide) (by decide) edge pair (edgeVertices k).1]
503 rw [freudenthalExplicitFiber_canonicalTetVerts_eq
504 (by decide) (by decide) (by decide) edge pair (edgeVertices k).2]
505
506/-- A total-order key for `N = 5` periodic vertices. This is used only to
507choose a canonical representative of an unordered monomial; the product order
508on `Fin 5 × Fin 5 × Fin 5` is partial and would drop incomparable pairs. -/
509def vertex5Code (v : Vertex5) : Nat :=
510 v.1.val * 25 + v.2.1.val * 5 + v.2.2.val
511
512theorem vertex5Code_injective : Function.Injective vertex5Code := by
513 intro a b h
514 rcases a with ⟨ax, ay, az⟩
515 rcases b with ⟨bx, by', bz⟩
516 ext <;> simp [vertex5Code] at h ⊢ <;> omega
517
518/-- Canonical total-order representative for unordered vertex pairs at `N = 5`. -/
519def vertex5CanonLE (u v : Vertex5) : Prop :=
520 vertex5Code u ≤ vertex5Code v
521
522instance (u v : Vertex5) : Decidable (vertex5CanonLE u v) :=
523 inferInstanceAs (Decidable (vertex5Code u ≤ vertex5Code v))
524
525/-- Unordered coefficient expansion for a diagonal monomial at `N = 5`.
526This is the square-term half of the axis-stencil soundness calculation. -/
527theorem unorderedDiagonalMonomialExpansionAtN5
528 (ξ : VertexPotential5) (a : Vertex5) (c : ℝ) :
529 (∑ u : Vertex5, ∑ v : Vertex5,
530 if vertex5CanonLE u v then
531 (if a = u && a = v then c * potentialAtVertex5 ξ u * potentialAtVertex5 ξ v else 0)
532 else 0) =
533 c * potentialAtVertex5 ξ a * potentialAtVertex5 ξ a := by
534 classical
535 rw [Finset.sum_eq_single a]
536 · rw [Finset.sum_eq_single a]
537 · simp [vertex5CanonLE]
538 · intro v _ hv
539 simp [hv.symm]
540 · intro hnot
541 exact (hnot (Finset.mem_univ a)).elim
542 · intro u _ hu
543 apply Finset.sum_eq_zero
544 intro v _
545 simp [hu.symm]
546 · intro hnot
547 exact (hnot (Finset.mem_univ a)).elim
548
549/-- Unordered coefficient expansion for an off-diagonal monomial at `N = 5`.
550This is the cross-term half of the axis-stencil soundness calculation. -/
551theorem unorderedCrossMonomialExpansionAtN5
552 (ξ : VertexPotential5) (a b : Vertex5) (c : ℝ) (hne : a ≠ b) :
553 (∑ u : Vertex5, ∑ v : Vertex5,
554 if vertex5CanonLE u v then
555 (if sameUnordered a b u v then
556 c * potentialAtVertex5 ξ u * potentialAtVertex5 ξ v
557 else 0)
558 else 0) =
559 c * potentialAtVertex5 ξ a * potentialAtVertex5 ξ b := by
560 classical
561 by_cases hab : vertex5CanonLE a b
562 · rw [Finset.sum_eq_single a]
563 · rw [Finset.sum_eq_single b]
564 · simp [sameUnordered, hab]
565 · intro v _ hv
566 by_cases huv : vertex5CanonLE a v
567 · by_cases hsu : sameUnordered a b a v
568 · have hp : (a = a ∧ b = v) ∨ (a = v ∧ b = a) := by
569 simpa [sameUnordered] using hsu
570 have hvb : v = b := by
571 rcases hp with ⟨_, hbv⟩ | ⟨_, hba⟩
572 · exact hbv.symm
573 · exact (hne hba.symm).elim
574 exact (hv hvb).elim
575 · simp [huv, hsu]
576 · simp [huv]
577 · intro hnot
578 exact (hnot (Finset.mem_univ b)).elim
579 · intro u _ hu
580 apply Finset.sum_eq_zero
581 intro v _
582 by_cases huv : vertex5CanonLE u v
583 · by_cases hsu : sameUnordered a b u v
584 · have hp : (a = u ∧ b = v) ∨ (a = v ∧ b = u) := by
585 simpa [sameUnordered] using hsu
586 rcases hp with ⟨hau, _⟩ | ⟨_, hbu⟩
587 · exact (hu hau.symm).elim
588 · subst u
589 subst v
590 exact (hne (vertex5Code_injective (le_antisymm hab huv))).elim
591 · simp [huv, hsu]
592 · simp [huv]
593 · intro hnot
594 exact (hnot (Finset.mem_univ a)).elim
595 · have hba : vertex5CanonLE b a := by
596 unfold vertex5CanonLE at hab ⊢
597 exact Nat.le_of_not_ge hab
598 rw [Finset.sum_eq_single b]
599 · rw [Finset.sum_eq_single a]
600 · simp [sameUnordered, hba]
601 ring
602 · intro v _ hv
603 by_cases huv : vertex5CanonLE b v
604 · by_cases hsu : sameUnordered a b b v
605 · have hp : (a = b ∧ b = v) ∨ (a = v ∧ b = b) := by
606 simpa [sameUnordered] using hsu
607 have hva : v = a := by
608 rcases hp with ⟨hab', _⟩ | ⟨hav, _⟩
609 · exact (hne hab').elim
610 · exact hav.symm
611 exact (hv hva).elim
612 · simp [huv, hsu]
613 · simp [huv]
614 · intro hnot
615 exact (hnot (Finset.mem_univ a)).elim
616 · intro u _ hu
617 apply Finset.sum_eq_zero
618 intro v _
619 by_cases huv : vertex5CanonLE u v
620 · by_cases hsu : sameUnordered a b u v
621 · have hp : (a = u ∧ b = v) ∨ (a = v ∧ b = u) := by
622 simpa [sameUnordered] using hsu
623 rcases hp with ⟨_, _⟩ | ⟨_, hbu⟩
624 · subst u
625 subst v
626 exact (hne (vertex5Code_injective (le_antisymm huv hba))).elim
627 · exact (hu hbu.symm).elim
628 · simp [huv, hsu]
629 · simp [huv]
630 · intro hnot
631 exact (hnot (Finset.mem_univ b)).elim
632
633/-- Unified unordered monomial expansion, valid also on the diagonal. This is
634the atom needed by the explicit-fiber LHS, where periodic wraparound can make
635many endpoint/local-vertex pairs incomparable in the product order. -/
636theorem unorderedSameUnorderedMonomialExpansionAtN5
637 (ξ : VertexPotential5) (a b : Vertex5) (c : ℝ) :
638 (∑ u : Vertex5, ∑ v : Vertex5,
639 if vertex5CanonLE u v then
640 (if sameUnordered a b u v then
641 c * potentialAtVertex5 ξ u * potentialAtVertex5 ξ v
642 else 0)
643 else 0) =
644 c * potentialAtVertex5 ξ a * potentialAtVertex5 ξ b := by
645 classical
646 by_cases h : a = b
647 · subst b
648 have hsame : ∀ u v : Vertex5, sameUnordered a a u v = (a = u && a = v) := by
649 intro u v
650 by_cases hu : a = u <;> by_cases hv : a = v <;>
651 simp [sameUnordered, hu, hv]
652 calc
653 (∑ u : Vertex5, ∑ v : Vertex5,
654 if vertex5CanonLE u v then
655 (if sameUnordered a a u v then
656 c * potentialAtVertex5 ξ u * potentialAtVertex5 ξ v
657 else 0)
658 else 0) =
659 (∑ u : Vertex5, ∑ v : Vertex5,
660 if vertex5CanonLE u v then
661 (if a = u && a = v then
662 c * potentialAtVertex5 ξ u * potentialAtVertex5 ξ v
663 else 0)
664 else 0) := by
665 refine Finset.sum_congr rfl ?_
666 intro u _
667 refine Finset.sum_congr rfl ?_
668 intro v _
669 by_cases huv : vertex5CanonLE u v <;> simp [huv, hsame u v]
670 _ = c * potentialAtVertex5 ξ a * potentialAtVertex5 ξ a :=
671 unorderedDiagonalMonomialExpansionAtN5 ξ a c
672 · exact unorderedCrossMonomialExpansionAtN5 ξ a b c h
673
674/-- One endpoint contribution from one explicit-fiber local pair and local edge
675slot expands to the two unordered monomials encoded by
676`scaledPairLocalVertexCoeff`. -/
677theorem scaledPairLocalVertexCoeffExpansionAtN5
678 (ξ : VertexPotential5) (edge : PeriodicEdge5) (pair : FreudenthalLocalPair)
679 (k : Fin 6) (endpoint : Vertex5) :
680 (∑ u : Vertex5, ∑ v : Vertex5,
681 if vertex5CanonLE u v then
682 ((scaledPairLocalVertexCoeff edge pair k endpoint u v : Rat) : ℝ) *
683 potentialAtVertex5 ξ u * potentialAtVertex5 ξ v
684 else 0) =
685 let cell := selectedCell5 edge pair
686 let ev := edgeVertices k
687 let v0 := addVertexBits cell (tetVerts pair.1 ev.1)
688 let v1 := addVertexBits cell (tetVerts pair.1 ev.2)
689 let c : ℝ := ((-(snormRat pair.2 k * sqEdgeRat k / 4) / 2 : Rat) : ℝ)
690 c * potentialAtVertex5 ξ endpoint * potentialAtVertex5 ξ v0 +
691 c * potentialAtVertex5 ξ endpoint * potentialAtVertex5 ξ v1 := by
692 classical
693 let cell := selectedCell5 edge pair
694 let ev := edgeVertices k
695 let v0 := addVertexBits cell (tetVerts pair.1 ev.1)
696 let v1 := addVertexBits cell (tetVerts pair.1 ev.2)
697 let cRat : Rat := -(snormRat pair.2 k * sqEdgeRat k / 4) / 2
698 let c : ℝ := (cRat : ℝ)
699 have h0 := unorderedSameUnorderedMonomialExpansionAtN5 ξ endpoint v0 c
700 have h1 := unorderedSameUnorderedMonomialExpansionAtN5 ξ endpoint v1 c
701 calc
702 (∑ u : Vertex5, ∑ v : Vertex5,
703 if vertex5CanonLE u v then
704 ((scaledPairLocalVertexCoeff edge pair k endpoint u v : Rat) : ℝ) *
705 potentialAtVertex5 ξ u * potentialAtVertex5 ξ v
706 else 0) =
707 (∑ u : Vertex5, ∑ v : Vertex5,
708 if vertex5CanonLE u v then
709 (if sameUnordered endpoint v0 u v then
710 c * potentialAtVertex5 ξ u * potentialAtVertex5 ξ v
711 else 0)
712 else 0) +
713 (∑ u : Vertex5, ∑ v : Vertex5,
714 if vertex5CanonLE u v then
715 (if sameUnordered endpoint v1 u v then
716 c * potentialAtVertex5 ξ u * potentialAtVertex5 ξ v
717 else 0)
718 else 0) := by
719 rw [← Finset.sum_add_distrib]
720 refine Finset.sum_congr rfl ?_
721 intro u _
722 rw [← Finset.sum_add_distrib]
723 refine Finset.sum_congr rfl ?_
724 intro v _
725 by_cases huv : vertex5CanonLE u v
726 · by_cases h0' : sameUnordered endpoint v0 u v
727 · by_cases h1' : sameUnordered endpoint v1 u v
728 · have h0raw :
729 sameUnordered endpoint
730 (addVertexBits (selectedCell5 edge pair)
731 (tetVerts pair.1 (edgeVertices k).1)) u v = true := by
732 simpa [cell, ev, v0] using h0'
733 have h1raw :
734 sameUnordered endpoint
735 (addVertexBits (selectedCell5 edge pair)
736 (tetVerts pair.1 (edgeVertices k).2)) u v = true := by
737 simpa [cell, ev, v1] using h1'
738 simp [scaledPairLocalVertexCoeff, cell, ev, v0, v1, c, cRat,
739 huv, h0', h1', h0raw, h1raw]
740 try ring_nf
741 · have h0raw :
742 sameUnordered endpoint
743 (addVertexBits (selectedCell5 edge pair)
744 (tetVerts pair.1 (edgeVertices k).1)) u v = true := by
745 simpa [cell, ev, v0] using h0'
746 have h1raw :
747 ¬ sameUnordered endpoint
748 (addVertexBits (selectedCell5 edge pair)
749 (tetVerts pair.1 (edgeVertices k).2)) u v = true := by
750 simpa [cell, ev, v1] using h1'
751 simp [scaledPairLocalVertexCoeff, cell, ev, v0, v1, c, cRat,
752 huv, h0', h1', h0raw, h1raw]
753 try ring_nf
754 · by_cases h1' : sameUnordered endpoint v1 u v
755 · have h0raw :
756 ¬ sameUnordered endpoint
757 (addVertexBits (selectedCell5 edge pair)
758 (tetVerts pair.1 (edgeVertices k).1)) u v = true := by
759 simpa [cell, ev, v0] using h0'
760 have h1raw :
761 sameUnordered endpoint
762 (addVertexBits (selectedCell5 edge pair)
763 (tetVerts pair.1 (edgeVertices k).2)) u v = true := by
764 simpa [cell, ev, v1] using h1'
765 simp [scaledPairLocalVertexCoeff, cell, ev, v0, v1, c, cRat,
766 huv, h0', h1', h0raw, h1raw]
767 try ring_nf
768 · have h0raw :
769 ¬ sameUnordered endpoint
770 (addVertexBits (selectedCell5 edge pair)
771 (tetVerts pair.1 (edgeVertices k).1)) u v = true := by
772 simpa [cell, ev, v0] using h0'
773 have h1raw :
774 ¬ sameUnordered endpoint
775 (addVertexBits (selectedCell5 edge pair)
776 (tetVerts pair.1 (edgeVertices k).2)) u v = true := by
777 simpa [cell, ev, v1] using h1'
778 simp [scaledPairLocalVertexCoeff, cell, ev, v0, v1, c, cRat,
779 huv, h0', h1', h0raw, h1raw]
780 try ring_nf
781 · simp [huv]
782 _ = c * potentialAtVertex5 ξ endpoint * potentialAtVertex5 ξ v0 +
783 c * potentialAtVertex5 ξ endpoint * potentialAtVertex5 ξ v1 := by
784 rw [h0, h1]
785 _ = (let cell := selectedCell5 edge pair
786 let ev := edgeVertices k
787 let v0 := addVertexBits cell (tetVerts pair.1 ev.1)
788 let v1 := addVertexBits cell (tetVerts pair.1 ev.2)
789 let c : ℝ := ((-(snormRat pair.2 k * sqEdgeRat k / 4) / 2 : Rat) : ℝ)
790 c * potentialAtVertex5 ξ endpoint * potentialAtVertex5 ξ v0 +
791 c * potentialAtVertex5 ξ endpoint * potentialAtVertex5 ξ v1) := by
792 simp [cell, ev, v0, v1, c, cRat]
793
794/-- The two endpoint contributions for one local pair and local edge slot expand
795by summing the endpoint-local atom theorem twice. -/
796theorem scaledPairLocalVertexCoeffEndpointSumExpansionAtN5
797 (ξ : VertexPotential5) (edge : PeriodicEdge5) (pair : FreudenthalLocalPair)
798 (k : Fin 6) (endpoint₀ endpoint₁ : Vertex5) :
799 (∑ u : Vertex5, ∑ v : Vertex5,
800 if vertex5CanonLE u v then
801 (((scaledPairLocalVertexCoeff edge pair k endpoint₀ u v +
802 scaledPairLocalVertexCoeff edge pair k endpoint₁ u v : Rat) : ℝ) *
803 potentialAtVertex5 ξ u * potentialAtVertex5 ξ v)
804 else 0) =
805 (let cell := selectedCell5 edge pair
806 let ev := edgeVertices k
807 let v0 := addVertexBits cell (tetVerts pair.1 ev.1)
808 let v1 := addVertexBits cell (tetVerts pair.1 ev.2)
809 let c : ℝ := ((-(snormRat pair.2 k * sqEdgeRat k / 4) / 2 : Rat) : ℝ)
810 c * potentialAtVertex5 ξ endpoint₀ * potentialAtVertex5 ξ v0 +
811 c * potentialAtVertex5 ξ endpoint₀ * potentialAtVertex5 ξ v1) +
812 (let cell := selectedCell5 edge pair
813 let ev := edgeVertices k
814 let v0 := addVertexBits cell (tetVerts pair.1 ev.1)
815 let v1 := addVertexBits cell (tetVerts pair.1 ev.2)
816 let c : ℝ := ((-(snormRat pair.2 k * sqEdgeRat k / 4) / 2 : Rat) : ℝ)
817 c * potentialAtVertex5 ξ endpoint₁ * potentialAtVertex5 ξ v0 +
818 c * potentialAtVertex5 ξ endpoint₁ * potentialAtVertex5 ξ v1) := by
819 classical
820 have h0 := scaledPairLocalVertexCoeffExpansionAtN5 ξ edge pair k endpoint₀
821 have h1 := scaledPairLocalVertexCoeffExpansionAtN5 ξ edge pair k endpoint₁
822 calc
823 (∑ u : Vertex5, ∑ v : Vertex5,
824 if vertex5CanonLE u v then
825 (((scaledPairLocalVertexCoeff edge pair k endpoint₀ u v +
826 scaledPairLocalVertexCoeff edge pair k endpoint₁ u v : Rat) : ℝ) *
827 potentialAtVertex5 ξ u * potentialAtVertex5 ξ v)
828 else 0) =
829 (∑ u : Vertex5, ∑ v : Vertex5,
830 if vertex5CanonLE u v then
831 ((scaledPairLocalVertexCoeff edge pair k endpoint₀ u v : Rat) : ℝ) *
832 potentialAtVertex5 ξ u * potentialAtVertex5 ξ v
833 else 0) +
834 (∑ u : Vertex5, ∑ v : Vertex5,
835 if vertex5CanonLE u v then
836 ((scaledPairLocalVertexCoeff edge pair k endpoint₁ u v : Rat) : ℝ) *
837 potentialAtVertex5 ξ u * potentialAtVertex5 ξ v
838 else 0) := by
839 rw [← Finset.sum_add_distrib]
840 refine Finset.sum_congr rfl ?_
841 intro u _
842 rw [← Finset.sum_add_distrib]
843 refine Finset.sum_congr rfl ?_
844 intro v _
845 by_cases huv : vertex5CanonLE u v
846 · simp [huv]
847 ring
848 · simp [huv]
849 _ = _ := by
850 rw [h0, h1]
851
852/-- Closed-form value produced by one endpoint/local-pair/local-slot coefficient
853atom after unordered monomial expansion. -/
854noncomputable def scaledPairEndpointExpansionValueAtN5
855 (ξ : VertexPotential5) (edge : PeriodicEdge5) (pair : FreudenthalLocalPair)
856 (k : Fin 6) (endpoint : Vertex5) : ℝ :=
857 let cell := selectedCell5 edge pair
858 let ev := edgeVertices k
859 let v0 := addVertexBits cell (tetVerts pair.1 ev.1)
860 let v1 := addVertexBits cell (tetVerts pair.1 ev.2)
861 let c : ℝ := ((-(snormRat pair.2 k * sqEdgeRat k / 4) / 2 : Rat) : ℝ)
862 c * potentialAtVertex5 ξ endpoint * potentialAtVertex5 ξ v0 +
863 c * potentialAtVertex5 ξ endpoint * potentialAtVertex5 ξ v1
864
865noncomputable def scaledPairEndpointSumExpansionValueAtN5
866 (ξ : VertexPotential5) (edge : PeriodicEdge5) (pair : FreudenthalLocalPair)
867 (k : Fin 6) (endpoint₀ endpoint₁ : Vertex5) : ℝ :=
868 scaledPairEndpointExpansionValueAtN5 ξ edge pair k endpoint₀ +
869 scaledPairEndpointExpansionValueAtN5 ξ edge pair k endpoint₁
870
871/-- One real explicit-fiber Schläfli/local-length slot equals the corresponding
872scaled coefficient atom after the edge/pair square-root cancellation. -/
873theorem explicitFiberMixedLhsSlot_scaledPairExpansionAtN5
874 (ξ : VertexPotential5) (edge : PeriodicEdge5) (pair : FreudenthalLocalPair)
875 (k : Fin 6) (hpair : pair ∈ freudenthalLocalPairDispFiber edge.disp) :
876 Geometry.ReggeActionFirstVariation.hingeMeasureDirectionalDeriv
877 P5.K P5.hK ξ (P5.edgeEquiv.symm edge) *
878 (-(freudenthalLocalPairClosedFormSchlaefliCoeff pair k *
879 freudenthalExplicitFiberFlatLocalEdgeLengthDirectionalDeriv
880 (by decide) (by decide) (by decide) ξ (selectedCell5 edge pair) pair.1 k)) =
881 scaledPairEndpointSumExpansionValueAtN5 ξ edge pair k
882 edge.endpoints.1 edge.endpoints.2 := by
883 classical
884 have hhinge :=
885 hingeMeasureDirectionalDeriv_canonicalEncodedPeriodic_edge
886 (Nx := 5) (Ny := 5) (Nz := 5)
887 (hx := by decide) (hy := by decide) (hz := by decide) ξ edge
888 have hlen :=
889 freudenthalExplicitFiberFlatLocalEdgeLengthDirectionalDeriv_selectedCell5 ξ edge pair k
890 have hsqDisp := periodicDispSqEdge_eq_freudenthalTetSqEdges_of_mem edge pair hpair
891 have hsqK_nonneg :
892 0 ≤ Geometry.FreudenthalCubeTriangulation.freudenthalTetSqEdges k := by
893 fin_cases k <;> norm_num [Geometry.FreudenthalCubeTriangulation.freudenthalTetSqEdges]
894 have hsqrK :
895 Real.sqrt (Geometry.FreudenthalCubeTriangulation.freudenthalTetSqEdges k) *
896 Real.sqrt (Geometry.FreudenthalCubeTriangulation.freudenthalTetSqEdges k) =
897 Geometry.FreudenthalCubeTriangulation.freudenthalTetSqEdges k := by
898 rw [← pow_two, Real.sq_sqrt hsqK_nonneg]
899 have hsqrK_pow :
900 Real.sqrt (Geometry.FreudenthalCubeTriangulation.freudenthalTetSqEdges k) ^ (2 : ℕ) =
901 Geometry.FreudenthalCubeTriangulation.freudenthalTetSqEdges k :=
902 Real.sq_sqrt hsqK_nonneg
903 have hsqrtPair_ne :
904 Real.sqrt (Geometry.FreudenthalCubeTriangulation.freudenthalTetSqEdges pair.2) ≠ 0 := by
905 apply ne_of_gt
906 apply Real.sqrt_pos.mpr
907 rcases pair with ⟨_tet, slot⟩
908 fin_cases slot <;> norm_num [Geometry.FreudenthalCubeTriangulation.freudenthalTetSqEdges]
909 rw [hhinge, hlen, freudenthalLocalPairClosedFormSchlaefliCoeff_eq_table]
910 rw [hsqDisp]
911 rw [← snormRat_cast_eq_freudenthalSchlaefliTable pair.2 k]
912 unfold scaledPairEndpointSumExpansionValueAtN5 scaledPairEndpointExpansionValueAtN5
913 potentialAtVertex5
914 field_simp [hsqrtPair_ne]
915 try simp
916 rw [hsqrK_pow, ← sqEdgeRat_cast_eq_freudenthalTetSqEdges k]
917 ring_nf
918
919/-- One explicit-fiber local pair contribution expands to the sum of its six
920checked endpoint-slot coefficient atoms. -/
921theorem explicitFiberMixedLhsPair_scaledPairExpansionAtN5
922 (ξ : VertexPotential5) (edge : PeriodicEdge5) (pair : FreudenthalLocalPair)
923 (hpair : pair ∈ freudenthalLocalPairDispFiber edge.disp) :
924 Geometry.ReggeActionFirstVariation.hingeMeasureDirectionalDeriv
925 P5.K P5.hK ξ (P5.edgeEquiv.symm edge) *
926 (-(freudenthalExplicitFiberPairExpandedSummand
927 (by decide) (by decide) (by decide) ξ edge pair)) =
928 ∑ k : Fin 6,
929 scaledPairEndpointSumExpansionValueAtN5 ξ edge pair k
930 edge.endpoints.1 edge.endpoints.2 := by
931 classical
932 have hclosed :
933 freudenthalExplicitFiberPairClosedFormExpandedSummand
934 (by decide) (by decide) (by decide) ξ edge pair =
935 freudenthalExplicitFiberPairExpandedSummand
936 (by decide) (by decide) (by decide) ξ edge pair :=
937 (freudenthalExplicitFiberPairClosedFormExpandedSummand_eq_flat
938 (by decide) (by decide) (by decide) ξ edge pair).trans
939 (freudenthalExplicitFiberPairFlatExpandedSummand_eq_expanded
940 (by decide) (by decide) (by decide) ξ edge pair)
941 rw [← hclosed]
942 unfold freudenthalExplicitFiberPairClosedFormExpandedSummand
943 freudenthalLocalPairClosedFormExpandedSummand
944 rw [← selectedCell5_eq_freudenthalExplicitFiberPairSelectedCell edge pair]
945 rw [← Finset.sum_neg_distrib, Finset.mul_sum]
946 refine Finset.sum_congr rfl ?_
947 intro k _
948 change
949 Geometry.ReggeActionFirstVariation.hingeMeasureDirectionalDeriv
950 P5.K P5.hK ξ (P5.edgeEquiv.symm edge) *
951 (-(freudenthalLocalPairClosedFormSchlaefliCoeff pair k *
952 freudenthalExplicitFiberFlatLocalEdgeLengthDirectionalDeriv
953 (by decide) (by decide) (by decide) ξ (selectedCell5 edge pair) pair.1 k)) =
954 scaledPairEndpointSumExpansionValueAtN5 ξ edge pair k
955 edge.endpoints.1 edge.endpoints.2
956 exact explicitFiberMixedLhsSlot_scaledPairExpansionAtN5 ξ edge pair k hpair
957
958/-- Edge-local real explicit-fiber LHS expansion against the checked endpoint-slot
959coefficient atoms. -/
960theorem explicitFiberMixedLhsEdge_scaledPairExpansionAtN5
961 (ξ : VertexPotential5) (edge : PeriodicEdge5) :
962 Geometry.ReggeActionFirstVariation.hingeMeasureDirectionalDeriv
963 P5.K P5.hK ξ (P5.edgeEquiv.symm edge) *
964 (-∑ pair ∈ freudenthalLocalPairDispFiber edge.disp,
965 freudenthalExplicitFiberPairExpandedSummand
966 (by decide) (by decide) (by decide) ξ edge pair) =
967 ∑ pair ∈ freudenthalLocalPairDispFiber edge.disp,
968 ∑ k : Fin 6,
969 scaledPairEndpointSumExpansionValueAtN5 ξ edge pair k
970 edge.endpoints.1 edge.endpoints.2 := by
971 classical
972 rw [← Finset.sum_neg_distrib, Finset.mul_sum]
973 refine Finset.sum_congr rfl ?_
974 intro pair hpair
975 exact explicitFiberMixedLhsPair_scaledPairExpansionAtN5 ξ edge pair hpair
976
977theorem scaledPairLocalVertexCoeffExpansionAtN5_value
978 (ξ : VertexPotential5) (edge : PeriodicEdge5) (pair : FreudenthalLocalPair)
979 (k : Fin 6) (endpoint : Vertex5) :
980 (∑ u : Vertex5, ∑ v : Vertex5,
981 if vertex5CanonLE u v then
982 ((scaledPairLocalVertexCoeff edge pair k endpoint u v : Rat) : ℝ) *
983 potentialAtVertex5 ξ u * potentialAtVertex5 ξ v
984 else 0) =
985 scaledPairEndpointExpansionValueAtN5 ξ edge pair k endpoint := by
986 simpa [scaledPairEndpointExpansionValueAtN5] using
987 scaledPairLocalVertexCoeffExpansionAtN5 ξ edge pair k endpoint
988
989theorem scaledPairLocalVertexCoeffEndpointSumExpansionAtN5_value
990 (ξ : VertexPotential5) (edge : PeriodicEdge5) (pair : FreudenthalLocalPair)
991 (k : Fin 6) (endpoint₀ endpoint₁ : Vertex5) :
992 (∑ u : Vertex5, ∑ v : Vertex5,
993 if vertex5CanonLE u v then
994 (((scaledPairLocalVertexCoeff edge pair k endpoint₀ u v +
995 scaledPairLocalVertexCoeff edge pair k endpoint₁ u v : Rat) : ℝ) *
996 potentialAtVertex5 ξ u * potentialAtVertex5 ξ v)
997 else 0) =
998 scaledPairEndpointSumExpansionValueAtN5 ξ edge pair k endpoint₀ endpoint₁ := by
999 simpa [scaledPairEndpointSumExpansionValueAtN5, scaledPairEndpointExpansionValueAtN5] using
1000 scaledPairLocalVertexCoeffEndpointSumExpansionAtN5 ξ edge pair k endpoint₀ endpoint₁
1001
1002/-- Edge-local LHS coefficient expansion: the unordered polynomial encoded by
1003`mixedAxisEdgeLhsCoeff edge` is the sum of the checked endpoint/local-slot atoms
1004for that edge. -/
1005theorem mixedAxisEdgeLhsCoeffExpansionAtN5
1006 (ξ : VertexPotential5) (edge : PeriodicEdge5) :
1007 (∑ u : Vertex5, ∑ v : Vertex5,
1008 if vertex5CanonLE u v then
1009 ((mixedAxisEdgeLhsCoeff edge u v : Rat) : ℝ) *
1010 potentialAtVertex5 ξ u * potentialAtVertex5 ξ v
1011 else 0) =
1012 ∑ pair ∈ freudenthalLocalPairDispFiber edge.disp,
1013 ∑ k : Fin 6,
1014 scaledPairEndpointSumExpansionValueAtN5 ξ edge pair k
1015 edge.endpoints.1 edge.endpoints.2 := by
1016 classical
1017 let F := fun (pair : FreudenthalLocalPair) (k : Fin 6) (u v : Vertex5) =>
1018 if vertex5CanonLE u v then
1019 (((scaledPairLocalVertexCoeff edge pair k edge.endpoints.1 u v +
1020 scaledPairLocalVertexCoeff edge pair k edge.endpoints.2 u v : Rat) : ℝ) *
1021 potentialAtVertex5 ξ u * potentialAtVertex5 ξ v)
1022 else 0
1023 have hdist :
1024 (∑ u : Vertex5, ∑ v : Vertex5,
1025 if vertex5CanonLE u v then
1026 ((mixedAxisEdgeLhsCoeff edge u v : Rat) : ℝ) *
1027 potentialAtVertex5 ξ u * potentialAtVertex5 ξ v
1028 else 0) =
1029 ∑ u : Vertex5, ∑ v : Vertex5,
1030 ∑ pair ∈ freudenthalLocalPairDispFiber edge.disp, ∑ k : Fin 6,
1031 F pair k u v := by
1032 unfold mixedAxisEdgeLhsCoeff
1033 refine Finset.sum_congr rfl ?_
1034 intro u _
1035 refine Finset.sum_congr rfl ?_
1036 intro v _
1037 by_cases huv : vertex5CanonLE u v
1038 · simp [F, huv, Finset.sum_mul]
1039 · simp [F, huv]
1040 have hreorder :
1041 (∑ u : Vertex5, ∑ v : Vertex5,
1042 ∑ pair ∈ freudenthalLocalPairDispFiber edge.disp, ∑ k : Fin 6,
1043 F pair k u v) =
1044 ∑ pair ∈ freudenthalLocalPairDispFiber edge.disp, ∑ k : Fin 6,
1045 ∑ u : Vertex5, ∑ v : Vertex5, F pair k u v := by
1046 calc
1047 (∑ u : Vertex5, ∑ v : Vertex5,
1048 ∑ pair ∈ freudenthalLocalPairDispFiber edge.disp, ∑ k : Fin 6,
1049 F pair k u v) =
1050 ∑ u : Vertex5, ∑ pair ∈ freudenthalLocalPairDispFiber edge.disp,
1051 ∑ v : Vertex5, ∑ k : Fin 6, F pair k u v := by
1052 refine Finset.sum_congr rfl ?_
1053 intro u _
1054 rw [Finset.sum_comm
1055 (s := (Finset.univ : Finset Vertex5))
1056 (t := freudenthalLocalPairDispFiber edge.disp)
1057 (f := fun v pair => ∑ k : Fin 6, F pair k u v)]
1058 _ =
1059 ∑ pair ∈ freudenthalLocalPairDispFiber edge.disp, ∑ u : Vertex5,
1060 ∑ v : Vertex5, ∑ k : Fin 6, F pair k u v := by
1061 rw [Finset.sum_comm
1062 (s := (Finset.univ : Finset Vertex5))
1063 (t := freudenthalLocalPairDispFiber edge.disp)
1064 (f := fun u pair => ∑ v : Vertex5, ∑ k : Fin 6, F pair k u v)]
1065 _ = ∑ pair ∈ freudenthalLocalPairDispFiber edge.disp, ∑ k : Fin 6,
1066 ∑ u : Vertex5, ∑ v : Vertex5, F pair k u v := by
1067 refine Finset.sum_congr rfl ?_
1068 intro pair _
1069 calc
1070 (∑ u : Vertex5, ∑ v : Vertex5, ∑ k : Fin 6, F pair k u v) =
1071 ∑ u : Vertex5, ∑ k : Fin 6, ∑ v : Vertex5, F pair k u v := by
1072 refine Finset.sum_congr rfl ?_
1073 intro u _
1074 rw [Finset.sum_comm
1075 (s := (Finset.univ : Finset Vertex5))
1076 (t := (Finset.univ : Finset (Fin 6)))
1077 (f := fun v k => F pair k u v)]
1078 _ = ∑ k : Fin 6, ∑ u : Vertex5, ∑ v : Vertex5, F pair k u v := by
1079 rw [Finset.sum_comm
1080 (s := (Finset.univ : Finset Vertex5))
1081 (t := (Finset.univ : Finset (Fin 6)))
1082 (f := fun u k => ∑ v : Vertex5, F pair k u v)]
1083 calc
1084 (∑ u : Vertex5, ∑ v : Vertex5,
1085 if vertex5CanonLE u v then
1086 ((mixedAxisEdgeLhsCoeff edge u v : Rat) : ℝ) *
1087 potentialAtVertex5 ξ u * potentialAtVertex5 ξ v
1088 else 0) =
1089 ∑ u : Vertex5, ∑ v : Vertex5,
1090 ∑ pair ∈ freudenthalLocalPairDispFiber edge.disp, ∑ k : Fin 6,
1091 F pair k u v := hdist
1092 _ = ∑ pair ∈ freudenthalLocalPairDispFiber edge.disp, ∑ k : Fin 6,
1093 ∑ u : Vertex5, ∑ v : Vertex5, F pair k u v := hreorder
1094 _ = ∑ pair ∈ freudenthalLocalPairDispFiber edge.disp, ∑ k : Fin 6,
1095 scaledPairEndpointSumExpansionValueAtN5 ξ edge pair k
1096 edge.endpoints.1 edge.endpoints.2 := by
1097 refine Finset.sum_congr rfl ?_
1098 intro pair _
1099 refine Finset.sum_congr rfl ?_
1100 intro k _
1101 simpa [F] using
1102 scaledPairLocalVertexCoeffEndpointSumExpansionAtN5_value
1103 ξ edge pair k edge.endpoints.1 edge.endpoints.2
1104
1105/-- On a five-periodic coordinate, adding one tick always remains comparable
1106with the starting point in the product order: either it moves forward without
1107wraparound, or it wraps from `4` to `0`. -/
1108theorem addBitTrueComparable5 (i : Fin 5) :
1109 i ≤ addBit i true ∨ addBit i true ≤ i := by
1110 fin_cases i <;> decide
1111
1112/-- Axis-edge endpoints in the `N = 5` periodic Freudenthal torus are comparable
1113in the product order. This remains useful for local geometry audits, although
1114the coefficient expansion now uses `vertex5CanonLE` to cover every unordered
1115pair on the periodic torus. -/
1116theorem axisEdgeEndpointsComparable5 (base : Vertex5) (d : Fin 3) :
1117 let edge : PeriodicEdge5 := { base := base, disp := periodicAxisDisp d }
1118 edge.endpoints.1 ≤ edge.endpoints.2 ∨ edge.endpoints.2 ≤ edge.endpoints.1 := by
1119 rcases base with ⟨x, y, z⟩
1120 fin_cases d
1121 · dsimp [PeriodicEdge.endpoints, periodicAxisDisp, dispBits, addBits]
1122 simp only [addBit_false]
1123 rcases addBitTrueComparable5 x with hx | hx
1124 · left
1125 constructor
1126 · exact hx
1127 · constructor <;> rfl
1128 · right
1129 constructor
1130 · exact hx
1131 · constructor <;> rfl
1132 · dsimp [PeriodicEdge.endpoints, periodicAxisDisp, dispBits, addBits]
1133 simp only [addBit_false]
1134 rcases addBitTrueComparable5 y with hy | hy
1135 · left
1136 constructor
1137 · rfl
1138 · constructor
1139 · exact hy
1140 · rfl
1141 · right
1142 constructor
1143 · rfl
1144 · constructor
1145 · exact hy
1146 · rfl
1147 · dsimp [PeriodicEdge.endpoints, periodicAxisDisp, dispBits, addBits]
1148 simp only [addBit_false]
1149 rcases addBitTrueComparable5 z with hz | hz
1150 · left
1151 constructor
1152 · rfl
1153 · constructor
1154 · rfl
1155 · exact hz
1156 · right
1157 constructor
1158 · rfl
1159 · constructor
1160 · rfl
1161 · exact hz
1162
1163set_option linter.unreachableTactic false
1164set_option linter.unusedTactic false
1165set_option linter.unnecessarySeqFocus false
1166
1167/-- The three local coefficient atoms for one non-loop axis edge
1168expand to the negative corrected Dirichlet contribution. -/
1169theorem pairAxisCoeffExpansionAtN5
1170 (ξ : VertexPotential5) (a b : Vertex5) (hne : a ≠ b) :
1171 (∑ u : Vertex5, ∑ v : Vertex5,
1172 if vertex5CanonLE u v then
1173 (((if a = u && a = v then (-2 : Rat) else 0) +
1174 (if b = u && b = v then (-2 : Rat) else 0) +
1175 (if sameUnordered a b u v then (4 : Rat) else 0) : Rat) : ℝ) *
1176 potentialAtVertex5 ξ u * potentialAtVertex5 ξ v
1177 else 0) =
1178 -2 * (potentialAtVertex5 ξ a - potentialAtVertex5 ξ b) ^ (2 : ℕ) := by
1179 classical
1180 have hdiagA := unorderedDiagonalMonomialExpansionAtN5 ξ a (-2)
1181 have hdiagB := unorderedDiagonalMonomialExpansionAtN5 ξ b (-2)
1182 have hcross := unorderedCrossMonomialExpansionAtN5 ξ a b 4 hne
1183 calc
1184 (∑ u : Vertex5, ∑ v : Vertex5,
1185 if vertex5CanonLE u v then
1186 (((if a = u && a = v then (-2 : Rat) else 0) +
1187 (if b = u && b = v then (-2 : Rat) else 0) +
1188 (if sameUnordered a b u v then (4 : Rat) else 0) : Rat) : ℝ) *
1189 potentialAtVertex5 ξ u * potentialAtVertex5 ξ v
1190 else 0) =
1191 (∑ u : Vertex5, ∑ v : Vertex5,
1192 if vertex5CanonLE u v then
1193 (if a = u && a = v then
1194 (-2 : ℝ) * potentialAtVertex5 ξ u * potentialAtVertex5 ξ v
1195 else 0)
1196 else 0) +
1197 (∑ u : Vertex5, ∑ v : Vertex5,
1198 if vertex5CanonLE u v then
1199 (if b = u && b = v then
1200 (-2 : ℝ) * potentialAtVertex5 ξ u * potentialAtVertex5 ξ v
1201 else 0)
1202 else 0) +
1203 (∑ u : Vertex5, ∑ v : Vertex5,
1204 if vertex5CanonLE u v then
1205 (if sameUnordered a b u v then
1206 (4 : ℝ) * potentialAtVertex5 ξ u * potentialAtVertex5 ξ v
1207 else 0)
1208 else 0) := by
1209 rw [← Finset.sum_add_distrib, ← Finset.sum_add_distrib]
1210 refine Finset.sum_congr rfl ?_
1211 intro u _
1212 rw [← Finset.sum_add_distrib, ← Finset.sum_add_distrib]
1213 refine Finset.sum_congr rfl ?_
1214 intro v _
1215 by_cases huv : vertex5CanonLE u v
1216 · by_cases ha : a = u && a = v
1217 · by_cases hb : b = u && b = v
1218 · by_cases hc : sameUnordered a b u v <;> simp [huv, ha, hb, hc] <;> ring
1219 · by_cases hc : sameUnordered a b u v <;> simp [huv, ha, hb, hc] <;> ring
1220 · by_cases hb : b = u && b = v
1221 · by_cases hc : sameUnordered a b u v <;> simp [huv, ha, hb, hc] <;> ring
1222 · by_cases hc : sameUnordered a b u v <;> simp [huv, ha, hb, hc] <;> ring
1223 · simp [huv]
1224 _ = (-2) * potentialAtVertex5 ξ a * potentialAtVertex5 ξ a +
1225 (-2) * potentialAtVertex5 ξ b * potentialAtVertex5 ξ b +
1226 4 * potentialAtVertex5 ξ a * potentialAtVertex5 ξ b := by
1227 rw [hdiagA, hdiagB, hcross]
1228 _ = -2 * (potentialAtVertex5 ξ a - potentialAtVertex5 ξ b) ^ (2 : ℕ) := by
1229 ring
1230
1231/-- Real-valued residual of the corrected explicit-fiber axis-stencil identity at
1232`N = 5`, written as `LHS - RHS`. -/
1233noncomputable def explicitFiberAxisStencilResidualAtN5 (ξ : VertexPotential5) : ℝ :=
1234 (∑ edge : PeriodicEdge5,
1235 let e := P5.edgeEquiv.symm edge
1236 Geometry.ReggeActionFirstVariation.hingeMeasureDirectionalDeriv P5.K P5.hK ξ e *
1237 (-∑ pair ∈ freudenthalLocalPairDispFiber edge.disp,
1238 freudenthalExplicitFiberPairExpandedSummand
1239 (by decide) (by decide) (by decide) ξ edge pair)) -
1240 canonicalPeriodicMixedAxisStencilAction 5 5 5 (by decide) (by decide) (by decide) ξ
1241
1242noncomputable def explicitFiberMixedLhsAtN5 (ξ : VertexPotential5) : ℝ :=
1243 ∑ edge : PeriodicEdge5,
1244 let e := P5.edgeEquiv.symm edge
1245 Geometry.ReggeActionFirstVariation.hingeMeasureDirectionalDeriv P5.K P5.hK ξ e *
1246 (-∑ pair ∈ freudenthalLocalPairDispFiber edge.disp,
1247 freudenthalExplicitFiberPairExpandedSummand
1248 (by decide) (by decide) (by decide) ξ edge pair)
1249
1250noncomputable def axisStencilResidualAtN5 (ξ : VertexPotential5) : ℝ :=
1251 -canonicalPeriodicMixedAxisStencilAction 5 5 5 (by decide) (by decide) (by decide) ξ
1252
1253theorem explicitFiberAxisStencilResidualAtN5_eq_lhs_add_axis
1254 (ξ : VertexPotential5) :
1255 explicitFiberAxisStencilResidualAtN5 ξ =
1256 explicitFiberMixedLhsAtN5 ξ + axisStencilResidualAtN5 ξ := by
1257 unfold explicitFiberAxisStencilResidualAtN5 explicitFiberMixedLhsAtN5 axisStencilResidualAtN5
1258 ring
1259
1260/-- Canonical unordered monomial expansion of the corrected rational residual
1261coefficient model. The Python audit indexes coefficients by unordered vertex
1262pairs; here `u ≤ v` gives the Lean-side canonical representative. -/
1263noncomputable def unorderedResidualCoeffExpansionAtN5 (ξ : VertexPotential5) : ℝ :=
1264 ∑ u : Vertex5, ∑ v : Vertex5,
1265 if vertex5CanonLE u v then
1266 (mixedAxisResidualCoeff u v : ℝ) * potentialAtVertex5 ξ u * potentialAtVertex5 ξ v
1267 else
1268 0
1269
1270noncomputable def unorderedLhsCoeffExpansionAtN5 (ξ : VertexPotential5) : ℝ :=
1271 ∑ u : Vertex5, ∑ v : Vertex5,
1272 if vertex5CanonLE u v then
1273 (mixedAxisLhsCoeff u v : ℝ) * potentialAtVertex5 ξ u * potentialAtVertex5 ξ v
1274 else
1275 0
1276
1277noncomputable def unorderedAxisCoeffExpansionAtN5 (ξ : VertexPotential5) : ℝ :=
1278 ∑ u : Vertex5, ∑ v : Vertex5,
1279 if vertex5CanonLE u v then
1280 (axisStencilResidualCoeff u v : ℝ) * potentialAtVertex5 ξ u * potentialAtVertex5 ξ v
1281 else
1282 0
1283
1284/-- Global coefficient-side LHS expansion, obtained by summing the edge-local
1285`mixedAxisEdgeLhsCoeffExpansionAtN5` theorem over all periodic edges. -/
1286theorem unorderedLhsCoeffExpansionAtN5_eq_edge_scaledPairSum
1287 (ξ : VertexPotential5) :
1288 unorderedLhsCoeffExpansionAtN5 ξ =
1289 ∑ edge : PeriodicEdge5,
1290 ∑ pair ∈ freudenthalLocalPairDispFiber edge.disp,
1291 ∑ k : Fin 6,
1292 scaledPairEndpointSumExpansionValueAtN5 ξ edge pair k
1293 edge.endpoints.1 edge.endpoints.2 := by
1294 classical
1295 let F := fun (edge : PeriodicEdge5) (u v : Vertex5) =>
1296 if vertex5CanonLE u v then
1297 ((mixedAxisEdgeLhsCoeff edge u v : Rat) : ℝ) *
1298 potentialAtVertex5 ξ u * potentialAtVertex5 ξ v
1299 else 0
1300 have hdist : unorderedLhsCoeffExpansionAtN5 ξ =
1301 ∑ u : Vertex5, ∑ v : Vertex5, ∑ edge : PeriodicEdge5, F edge u v := by
1302 unfold unorderedLhsCoeffExpansionAtN5 mixedAxisLhsCoeff
1303 refine Finset.sum_congr rfl ?_
1304 intro u _
1305 refine Finset.sum_congr rfl ?_
1306 intro v _
1307 by_cases huv : vertex5CanonLE u v
1308 · simp [F, huv, Finset.sum_mul]
1309 · simp [F, huv]
1310 have hreorder :
1311 (∑ u : Vertex5, ∑ v : Vertex5, ∑ edge : PeriodicEdge5, F edge u v) =
1312 ∑ edge : PeriodicEdge5, ∑ u : Vertex5, ∑ v : Vertex5, F edge u v := by
1313 calc
1314 (∑ u : Vertex5, ∑ v : Vertex5, ∑ edge : PeriodicEdge5, F edge u v) =
1315 ∑ u : Vertex5, ∑ edge : PeriodicEdge5, ∑ v : Vertex5, F edge u v := by
1316 refine Finset.sum_congr rfl ?_
1317 intro u _
1318 rw [Finset.sum_comm
1319 (s := (Finset.univ : Finset Vertex5))
1320 (t := (Finset.univ : Finset PeriodicEdge5))
1321 (f := fun v edge => F edge u v)]
1322 _ = ∑ edge : PeriodicEdge5, ∑ u : Vertex5, ∑ v : Vertex5, F edge u v := by
1323 rw [Finset.sum_comm
1324 (s := (Finset.univ : Finset Vertex5))
1325 (t := (Finset.univ : Finset PeriodicEdge5))
1326 (f := fun u edge => ∑ v : Vertex5, F edge u v)]
1327 calc
1328 unorderedLhsCoeffExpansionAtN5 ξ =
1329 ∑ u : Vertex5, ∑ v : Vertex5, ∑ edge : PeriodicEdge5, F edge u v := hdist
1330 _ = ∑ edge : PeriodicEdge5, ∑ u : Vertex5, ∑ v : Vertex5, F edge u v := hreorder
1331 _ = ∑ edge : PeriodicEdge5,
1332 ∑ pair ∈ freudenthalLocalPairDispFiber edge.disp,
1333 ∑ k : Fin 6,
1334 scaledPairEndpointSumExpansionValueAtN5 ξ edge pair k
1335 edge.endpoints.1 edge.endpoints.2 := by
1336 refine Finset.sum_congr rfl ?_
1337 intro edge _
1338 simpa [F] using mixedAxisEdgeLhsCoeffExpansionAtN5 ξ edge
1339
1340theorem unorderedResidualCoeffExpansionAtN5_eq_lhs_add_axis
1341 (ξ : VertexPotential5) :
1342 unorderedResidualCoeffExpansionAtN5 ξ =
1343 unorderedLhsCoeffExpansionAtN5 ξ + unorderedAxisCoeffExpansionAtN5 ξ := by
1344 unfold unorderedResidualCoeffExpansionAtN5 unorderedLhsCoeffExpansionAtN5
1345 unorderedAxisCoeffExpansionAtN5 mixedAxisResidualCoeff
1346 rw [← Finset.sum_add_distrib]
1347 refine Finset.sum_congr rfl ?_
1348 intro u _
1349 rw [← Finset.sum_add_distrib]
1350 refine Finset.sum_congr rfl ?_
1351 intro v _
1352 by_cases huv : vertex5CanonLE u v
1353 · simp [huv]
1354 ring
1355 · simp [huv]
1356
1357/-- Global real explicit-fiber LHS expansion over the same edge/pair/slot atoms
1358used by the coefficient-side theorem. -/
1359theorem explicitFiberMixedLhsAtN5_eq_edge_scaledPairSum
1360 (ξ : VertexPotential5) :
1361 explicitFiberMixedLhsAtN5 ξ =
1362 ∑ edge : PeriodicEdge5,
1363 ∑ pair ∈ freudenthalLocalPairDispFiber edge.disp,
1364 ∑ k : Fin 6,
1365 scaledPairEndpointSumExpansionValueAtN5 ξ edge pair k
1366 edge.endpoints.1 edge.endpoints.2 := by
1367 classical
1368 unfold explicitFiberMixedLhsAtN5
1369 refine Finset.sum_congr rfl ?_
1370 intro edge _
1371 simpa using explicitFiberMixedLhsEdge_scaledPairExpansionAtN5 ξ edge
1372
1373def ExplicitFiberMixedLhsCoeffSoundnessAtN5 : Prop :=
1374 ∀ ξ : VertexPotential5,
1375 explicitFiberMixedLhsAtN5 ξ = unorderedLhsCoeffExpansionAtN5 ξ
1376
1377/-- The real explicit-fiber mixed LHS and the rational unordered LHS coefficient
1378model are the same quadratic form at `N = 5`. -/
1379theorem explicitFiberMixedLhsCoeffSoundnessAtN5 :
1380 ExplicitFiberMixedLhsCoeffSoundnessAtN5 := by
1381 intro ξ
1382 rw [explicitFiberMixedLhsAtN5_eq_edge_scaledPairSum,
1383 unorderedLhsCoeffExpansionAtN5_eq_edge_scaledPairSum]
1384
1385def AxisStencilCoeffSoundnessAtN5 : Prop :=
1386 ∀ ξ : VertexPotential5,
1387 axisStencilResidualAtN5 ξ = unorderedAxisCoeffExpansionAtN5 ξ
1388
1389/-- The corrected three-axis stencil is sound with respect to the unordered
1390coefficient expansion. This closes the RHS half of
1391`ExplicitFiberAxisStencilCoeffSoundnessAtN5`; the remaining packaging work is
1392the explicit-fiber LHS expansion. -/
1393theorem axisStencilCoeffSoundnessAtN5 :
1394 AxisStencilCoeffSoundnessAtN5 := by
1395 intro ξ
1396 let atom := fun (base : Vertex5) (d : Fin 3) (u v : Vertex5) =>
1397 let edge : PeriodicEdge5 := { base := base, disp := periodicAxisDisp d }
1398 let ep := edge.endpoints
1399 (if ep.1 = u && ep.1 = v then (-2 : Rat) else 0) +
1400 (if ep.2 = u && ep.2 = v then (-2 : Rat) else 0) +
1401 (if sameUnordered ep.1 ep.2 u v then (4 : Rat) else 0)
1402 let F := fun (u v base : Vertex5) (d : Fin 3) =>
1403 if vertex5CanonLE u v then ((atom base d u v : Rat) : ℝ) *
1404 potentialAtVertex5 ξ u * potentialAtVertex5 ξ v else 0
1405 have hdist : unorderedAxisCoeffExpansionAtN5 ξ =
1406 ∑ u : Vertex5, ∑ v : Vertex5, ∑ base : Vertex5, ∑ d : Fin 3,
1407 F u v base d := by
1408 unfold unorderedAxisCoeffExpansionAtN5 axisStencilResidualCoeff
1409 refine Finset.sum_congr rfl ?_
1410 intro u _
1411 refine Finset.sum_congr rfl ?_
1412 intro v _
1413 by_cases huv : vertex5CanonLE u v
1414 · simp only [huv, if_true, F]
1415 simp [atom, Finset.sum_mul]
1416 · simp [F, huv]
1417 have hreorder :
1418 (∑ u : Vertex5, ∑ v : Vertex5, ∑ base : Vertex5, ∑ d : Fin 3,
1419 F u v base d) =
1420 ∑ base : Vertex5, ∑ d : Fin 3, ∑ u : Vertex5, ∑ v : Vertex5,
1421 F u v base d := by
1422 calc
1423 (∑ u : Vertex5, ∑ v : Vertex5, ∑ base : Vertex5, ∑ d : Fin 3,
1424 F u v base d) =
1425 ∑ u : Vertex5, ∑ base : Vertex5, ∑ v : Vertex5, ∑ d : Fin 3,
1426 F u v base d := by
1427 refine Finset.sum_congr rfl ?_
1428 intro u _
1429 rw [@Finset.sum_comm Vertex5 ℝ Vertex5 _
1430 (s := Finset.univ) (t := Finset.univ)
1431 (f := fun v base => ∑ d : Fin 3, F u v base d)]
1432 _ = ∑ base : Vertex5, ∑ u : Vertex5, ∑ v : Vertex5, ∑ d : Fin 3,
1433 F u v base d := by
1434 rw [@Finset.sum_comm Vertex5 ℝ Vertex5 _
1435 (s := Finset.univ) (t := Finset.univ)
1436 (f := fun u base => ∑ v : Vertex5, ∑ d : Fin 3, F u v base d)]
1437 _ = ∑ base : Vertex5, ∑ d : Fin 3, ∑ u : Vertex5, ∑ v : Vertex5,
1438 F u v base d := by
1439 refine Finset.sum_congr rfl ?_
1440 intro base _
1441 calc
1442 (∑ u : Vertex5, ∑ v : Vertex5, ∑ d : Fin 3,
1443 F u v base d) =
1444 ∑ u : Vertex5, ∑ d : Fin 3, ∑ v : Vertex5,
1445 F u v base d := by
1446 refine Finset.sum_congr rfl ?_
1447 intro u _
1448 rw [@Finset.sum_comm (Fin 3) ℝ Vertex5 _
1449 (s := Finset.univ) (t := Finset.univ)
1450 (f := fun v d => F u v base d)]
1451 _ = ∑ d : Fin 3, ∑ u : Vertex5, ∑ v : Vertex5,
1452 F u v base d := by
1453 rw [@Finset.sum_comm (Fin 3) ℝ Vertex5 _
1454 (s := Finset.univ) (t := Finset.univ)
1455 (f := fun u d => ∑ v : Vertex5, F u v base d)]
1456 have hpairSum :
1457 (∑ base : Vertex5, ∑ d : Fin 3, ∑ u : Vertex5, ∑ v : Vertex5,
1458 F u v base d) =
1459 ∑ base : Vertex5, ∑ d : Fin 3,
1460 -2 * (potentialAtVertex5 ξ
1461 ({ base := base, disp := periodicAxisDisp d } : PeriodicEdge5).endpoints.1 -
1462 potentialAtVertex5 ξ
1463 ({ base := base, disp := periodicAxisDisp d } : PeriodicEdge5).endpoints.2) ^ (2 : ℕ) := by
1464 refine Finset.sum_congr rfl ?_
1465 intro base _
1466 refine Finset.sum_congr rfl ?_
1467 intro d _
1468 let edge : PeriodicEdge5 := { base := base, disp := periodicAxisDisp d }
1469 have hne : edge.endpoints.1 ≠ edge.endpoints.2 :=
1470 PeriodicEdge.endpoints_ne (by decide) (by decide) (by decide) edge
1471 simpa [F, atom, edge] using
1472 pairAxisCoeffExpansionAtN5 ξ edge.endpoints.1 edge.endpoints.2 hne
1473 have hcoeff : unorderedAxisCoeffExpansionAtN5 ξ =
1474 ∑ base : Vertex5, ∑ d : Fin 3,
1475 -2 * (potentialAtVertex5 ξ
1476 ({ base := base, disp := periodicAxisDisp d } : PeriodicEdge5).endpoints.1 -
1477 potentialAtVertex5 ξ
1478 ({ base := base, disp := periodicAxisDisp d } : PeriodicEdge5).endpoints.2) ^ (2 : ℕ) := by
1479 rw [hdist, hreorder, hpairSum]
1480 have haxis : axisStencilResidualAtN5 ξ =
1481 ∑ base : Vertex5, ∑ d : Fin 3,
1482 -2 * (potentialAtVertex5 ξ
1483 ({ base := base, disp := periodicAxisDisp d } : PeriodicEdge5).endpoints.1 -
1484 potentialAtVertex5 ξ
1485 ({ base := base, disp := periodicAxisDisp d } : PeriodicEdge5).endpoints.2) ^ (2 : ℕ) := by
1486 unfold axisStencilResidualAtN5 canonicalPeriodicMixedAxisStencilAction potentialAtVertex5
1487 rw [← Finset.sum_neg_distrib]
1488 refine Finset.sum_congr rfl ?_
1489 intro base _
1490 rw [← Finset.sum_neg_distrib]
1491 refine Finset.sum_congr rfl ?_
1492 intro d _
1493 ring
1494 rw [haxis, hcoeff]
1495
1496/-- Coefficient-soundness bridge for the corrected `N = 5` certificate: the real
1497explicit-fiber residual is the unordered monomial expansion of the rational
1498residual coefficients. This is the remaining algebraic packaging surface after
1499Session 212 closed every coefficient. -/
1500def ExplicitFiberAxisStencilCoeffSoundnessAtN5 : Prop :=
1501 ∀ ξ : VertexPotential5,
1502 explicitFiberAxisStencilResidualAtN5 ξ = unorderedResidualCoeffExpansionAtN5 ξ
1503
1504theorem ExplicitFiberAxisStencilCoeffSoundnessAtN5_of_parts
1505 (hlhs : ExplicitFiberMixedLhsCoeffSoundnessAtN5)
1506 (haxis : AxisStencilCoeffSoundnessAtN5) :
1507 ExplicitFiberAxisStencilCoeffSoundnessAtN5 := by
1508 intro ξ
1509 rw [explicitFiberAxisStencilResidualAtN5_eq_lhs_add_axis,
1510 unorderedResidualCoeffExpansionAtN5_eq_lhs_add_axis, hlhs ξ, haxis ξ]
1511
1512/-- Combined coefficient-soundness theorem for the corrected explicit-fiber
1513axis-stencil residual at `N = 5`. -/
1514theorem explicitFiberAxisStencilCoeffSoundnessAtN5 :
1515 ExplicitFiberAxisStencilCoeffSoundnessAtN5 :=
1516 ExplicitFiberAxisStencilCoeffSoundnessAtN5_of_parts
1517 explicitFiberMixedLhsCoeffSoundnessAtN5
1518 axisStencilCoeffSoundnessAtN5
1519
1520theorem fullResidualCoeffCert_unordered_expansion_zero
1521 (hcoeff : FullResidualCoeffCert) (ξ : VertexPotential5) :
1522 unorderedResidualCoeffExpansionAtN5 ξ = 0 := by
1523 unfold unorderedResidualCoeffExpansionAtN5
1524 apply Finset.sum_eq_zero
1525 intro u _
1526 apply Finset.sum_eq_zero
1527 intro v _
1528 by_cases huv : vertex5CanonLE u v
1529 · simp [huv, hcoeff u v]
1530 · simp [huv]
1531
1532/-- Packaging reduction from the coefficient certificate to the corrected
1533explicit-fiber axis-stencil target. The only remaining input is the algebraic
1534soundness theorem identifying the real residual with the coefficient model. -/
1535theorem canonicalPeriodicMixedHingeDeficitExplicitFiberAxisStencilTargetAtN5_of_coeffSoundness
1536 (hsound : ExplicitFiberAxisStencilCoeffSoundnessAtN5) :
1537 CanonicalPeriodicMixedHingeDeficitExplicitFiberAxisStencilTargetAtN5 := by
1538 intro ξ
1539 have hres := hsound ξ
1540 have hzero : unorderedResidualCoeffExpansionAtN5 ξ = 0 :=
1541 fullResidualCoeffCert_unordered_expansion_zero fullResidualCoeffCert ξ
1542 have hdiff : explicitFiberAxisStencilResidualAtN5 ξ = 0 := by
1543 rw [hres, hzero]
1544 unfold explicitFiberAxisStencilResidualAtN5 at hdiff
1545 exact sub_eq_zero.mp hdiff
1546
1547theorem canonicalPeriodicMixedHingeDeficitAxisStencilTargetAtN5_of_coeffSoundness
1548 (hsound : ExplicitFiberAxisStencilCoeffSoundnessAtN5) :
1549 CanonicalPeriodicMixedHingeDeficitAxisStencilTargetAtN5 :=
1550 canonicalPeriodicMixedHingeDeficitAxisStencilTargetAtN5_of_explicitFiberAxis
1551 (canonicalPeriodicMixedHingeDeficitExplicitFiberAxisStencilTargetAtN5_of_coeffSoundness hsound)
1552
1553/-- Closed corrected explicit-fiber axis-stencil target at `N = 5`, obtained
1554from the finite coefficient certificate and the real/coefficient soundness
1555bridge. -/
1556theorem canonicalPeriodicMixedHingeDeficitExplicitFiberAxisStencilTargetAtN5 :
1557 CanonicalPeriodicMixedHingeDeficitExplicitFiberAxisStencilTargetAtN5 :=
1558 canonicalPeriodicMixedHingeDeficitExplicitFiberAxisStencilTargetAtN5_of_coeffSoundness
1559 explicitFiberAxisStencilCoeffSoundnessAtN5
1560
1561/-- Closed corrected mixed axis-stencil target at `N = 5`, via the explicit-fiber
1562wrapper. -/
1563theorem canonicalPeriodicMixedHingeDeficitAxisStencilTargetAtN5 :
1564 CanonicalPeriodicMixedHingeDeficitAxisStencilTargetAtN5 :=
1565 canonicalPeriodicMixedHingeDeficitAxisStencilTargetAtN5_of_coeffSoundness
1566 explicitFiberAxisStencilCoeffSoundnessAtN5
1567
1568theorem rowMixedAxisLhsCoeffTranslationInvariant_100_eq_true :
1569 rowMixedAxisLhsCoeffTranslationInvariant (1, 0, 0) = true := by
1570 native_decide
1571
1572def rowResidualCoeffsZero (u : Vertex5) : Bool :=
1573 decide (∀ v : Vertex5, mixedAxisResidualCoeff u v = 0)
1574
1575theorem rowResidualCoeffsZero_100_eq_true :
1576 rowResidualCoeffsZero (1, 0, 0) = true := by
1577 native_decide
1578
1579end FreudenthalAxisStencilCoeffCert
1580end Gravity
1581end IndisputableMonolith
1582