IndisputableMonolith.Geometry.ReggeActionConcrete
IndisputableMonolith/Geometry/ReggeActionConcrete.lean · 677 lines · 45 declarations
show as:
view math explainer →
1import Mathlib.Analysis.SpecialFunctions.Exp
2import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
3import IndisputableMonolith.Geometry.ReggeHessian3D
4import IndisputableMonolith.Geometry.Triangulation3DConsistency
5import IndisputableMonolith.Geometry.DihedralDerivatives
6
7/-!
8# Concrete Regge Action Hessian Target
9
10This module isolates the final analytic Hessian step for a finite 3D Regge
11triangulation. A concrete action package supplies the Regge action under the
12conformal ansatz and proves its second variation; the module turns that into
13the existing `ReggeHessianData` interface.
14-/
15
16namespace IndisputableMonolith
17namespace Geometry
18namespace ReggeActionConcrete
19
20open ReggeTriangulation3D
21open ReggeHessian3D
22open Triangulation3DConsistency
23open DihedralDerivatives
24
25noncomputable section
26
27/-- Local squared-edge data in tetrahedron `τ` under the vertex-conformal
28ansatz. The local edge `f = (u,v)` scales by `exp (ξ_u + ξ_v)`. -/
29def conformalLocalSqEdge
30 (K : Triangulation3D) (ξ : VertexPotential K)
31 (τ : Fin K.nT) (f : Fin 6) : ℝ :=
32 let uv := ReggeRigorousFoundation.edgeVertices f
33 (K.tet τ).sqEdge f *
34 Real.exp (ξ (K.tetVerts τ uv.1) + ξ (K.tetVerts τ uv.2))
35
36/-- The six conformally scaled squared-edge coordinates of a tetrahedron. -/
37def conformalTetSqEdges
38 (K : Triangulation3D) (ξ : VertexPotential K) (τ : Fin K.nT) :
39 CayleyMengerPolynomial.SqEdges :=
40 fun f => conformalLocalSqEdge K ξ τ f
41
42/-- Dihedral angle of a local tetrahedral edge under the conformal ansatz,
43computed directly from the Cayley-Menger cofactor formula on squared-edge
44data. -/
45def tetDihedralAngleUnderConformal
46 (K : Triangulation3D) (ξ : VertexPotential K)
47 (τ : Fin K.nT) (f : Fin 6) : ℝ :=
48 dihedralAngle3Sq (conformalTetSqEdges K ξ τ) f
49
50/-- A local incidence contribution to the deficit angle at a global edge. -/
51def localDeficitAngleContribution
52 (K : Triangulation3D) (ξ : VertexPotential K)
53 (e : Fin K.nE) (τ : Fin K.nT) : ℝ :=
54 match K.edgeInTet e τ with
55 | some f => tetDihedralAngleUnderConformal K ξ τ f
56 | none => 0
57
58/-- Regge deficit angle at a global edge under the conformal ansatz. -/
59def deficitAngle
60 (K : Triangulation3D) (ξ : VertexPotential K) (e : Fin K.nE) : ℝ :=
61 2 * Real.pi - ∑ τ : Fin K.nT, localDeficitAngleContribution K ξ e τ
62
63/-- The 3D Regge hinge measure is the edge length. This is the conformal
64length of a global edge under the vertex-conformal ansatz. -/
65def hingeMeasureUnderConformal
66 (K : Triangulation3D) (hK : IncidenceConsistent K)
67 (ξ : VertexPotential K) (e : Fin K.nE) : ℝ :=
68 let uv := K.edgeVerts e
69 Real.sqrt (hK.globalSqEdge e) *
70 Real.exp ((ξ uv.1 + ξ uv.2) / 2)
71
72/-- The concrete 3D Regge action under the vertex-conformal ansatz. -/
73def reggeAction
74 (K : Triangulation3D) (hK : IncidenceConsistent K)
75 (ξ : VertexPotential K) : ℝ :=
76 ∑ e : Fin K.nE,
77 hingeMeasureUnderConformal K hK ξ e * deficitAngle K ξ e
78
79/-- The quadratic second-order truncation associated with a candidate Hessian
80matrix. This is the object for which exact quadratic second-variation
81statements are definitionally correct; the full nonlinear action needs a
82Taylor remainder theorem. -/
83def reggeActionSecondOrder
84 (K : Triangulation3D) (hK : IncidenceConsistent K)
85 (H : Fin K.nV → Fin K.nV → ℝ)
86 (ξ : VertexPotential K) : ℝ :=
87 reggeAction K hK (zeroPotential K) + (1 / 2) * hessianQuadratic H ξ
88
89/-- The nonlinear Taylor remainder after subtracting the value at zero and a
90candidate quadratic Hessian term from the full Regge action. -/
91def reggeActionRemainder
92 (K : Triangulation3D) (hK : IncidenceConsistent K)
93 (H : Fin K.nV → Fin K.nV → ℝ)
94 (ξ : VertexPotential K) : ℝ :=
95 reggeAction K hK ξ - reggeAction K hK (zeroPotential K) -
96 (1 / 2) * hessianQuadratic H ξ
97
98theorem hessianQuadratic_zeroPotential
99 (K : Triangulation3D) (H : Fin K.nV → Fin K.nV → ℝ) :
100 hessianQuadratic H (zeroPotential K) = 0 := by
101 unfold hessianQuadratic zeroPotential
102 simp
103
104/-- Exact decomposition of the nonlinear action into its value at zero, a
105candidate quadratic Hessian term, and the remaining nonlinear part. -/
106theorem reggeAction_taylor_decomposition
107 (K : Triangulation3D) (hK : IncidenceConsistent K)
108 (H : Fin K.nV → Fin K.nV → ℝ)
109 (ξ : VertexPotential K) :
110 reggeAction K hK ξ =
111 reggeAction K hK (zeroPotential K) +
112 (1 / 2) * hessianQuadratic H ξ +
113 reggeActionRemainder K hK H ξ := by
114 unfold reggeActionRemainder
115 ring
116
117/-- The nonlinear remainder vanishes at the flat potential, for every
118candidate Hessian. -/
119theorem reggeActionRemainder_zero
120 (K : Triangulation3D) (hK : IncidenceConsistent K)
121 (H : Fin K.nV → Fin K.nV → ℝ) :
122 reggeActionRemainder K hK H (zeroPotential K) = 0 := by
123 unfold reggeActionRemainder
124 rw [hessianQuadratic_zeroPotential K H]
125 ring
126
127/-- Exact second variation of the quadratic truncation. -/
128theorem reggeActionSecondOrder_secondVariation
129 (K : Triangulation3D) (hK : IncidenceConsistent K)
130 (H : Fin K.nV → Fin K.nV → ℝ) (ξ : VertexPotential K) :
131 reggeActionSecondOrder K hK H ξ -
132 reggeActionSecondOrder K hK H (zeroPotential K) =
133 (1 / 2) * hessianQuadratic H ξ := by
134 unfold reggeActionSecondOrder
135 have hzero : hessianQuadratic H (zeroPotential K) = 0 :=
136 hessianQuadratic_zeroPotential K H
137 rw [hzero]
138 ring
139
140/-- A global edge contributes to the unordered vertex pair `(i,j)` when its
141endpoints are `(i,j)` or `(j,i)`. -/
142def canonicalEdgePairWeight
143 (K : Triangulation3D) (hK : IncidenceConsistent K)
144 (i j : Fin K.nV) (e : Fin K.nE) : ℝ :=
145 if (K.edgeVerts e).1 = i ∧ (K.edgeVerts e).2 = j ∨
146 (K.edgeVerts e).1 = j ∧ (K.edgeVerts e).2 = i then
147 Real.sqrt (hK.globalSqEdge e)
148 else
149 0
150
151/-- Incidence-defined vertex-pair hinge weight. -/
152def canonicalDualWeight
153 (K : Triangulation3D) (hK : IncidenceConsistent K)
154 (i j : Fin K.nV) : ℝ :=
155 ∑ e : Fin K.nE, canonicalEdgePairWeight K hK i j e
156
157theorem canonicalEdgePairWeight_symm
158 (K : Triangulation3D) (hK : IncidenceConsistent K)
159 (i j : Fin K.nV) (e : Fin K.nE) :
160 canonicalEdgePairWeight K hK i j e =
161 canonicalEdgePairWeight K hK j i e := by
162 unfold canonicalEdgePairWeight
163 by_cases h :
164 (K.edgeVerts e).1 = i ∧ (K.edgeVerts e).2 = j ∨
165 (K.edgeVerts e).1 = j ∧ (K.edgeVerts e).2 = i
166 · have h' :
167 (K.edgeVerts e).1 = j ∧ (K.edgeVerts e).2 = i ∨
168 (K.edgeVerts e).1 = i ∧ (K.edgeVerts e).2 = j := h.symm
169 simp [h, h']
170 · have h' :
171 ¬ ((K.edgeVerts e).1 = j ∧ (K.edgeVerts e).2 = i ∨
172 (K.edgeVerts e).1 = i ∧ (K.edgeVerts e).2 = j) := by
173 intro hx
174 exact h hx.symm
175 simp [h, h']
176
177theorem canonicalDualWeight_symm
178 (K : Triangulation3D) (hK : IncidenceConsistent K) :
179 ∀ i j, canonicalDualWeight K hK i j = canonicalDualWeight K hK j i := by
180 intro i j
181 unfold canonicalDualWeight
182 exact Finset.sum_congr rfl (fun e _ => canonicalEdgePairWeight_symm K hK i j e)
183
184theorem canonicalDualWeight_nonneg
185 (K : Triangulation3D) (hK : IncidenceConsistent K) :
186 ∀ i j, 0 ≤ canonicalDualWeight K hK i j := by
187 intro i j
188 unfold canonicalDualWeight canonicalEdgePairWeight
189 refine Finset.sum_nonneg ?_
190 intro e _
191 by_cases h :
192 (K.edgeVerts e).1 = i ∧ (K.edgeVerts e).2 = j ∨
193 (K.edgeVerts e).1 = j ∧ (K.edgeVerts e).2 = i
194 · simp [h, Real.sqrt_nonneg]
195 · simp [h]
196
197/-- Canonical graph-Laplacian Hessian induced by incidence dual weights. -/
198def canonicalReggeHessian
199 (K : Triangulation3D) (hK : IncidenceConsistent K)
200 (i j : Fin K.nV) : ℝ :=
201 (if i = j then ∑ k : Fin K.nV, canonicalDualWeight K hK i k else 0)
202 - canonicalDualWeight K hK i j
203
204theorem canonicalReggeHessian_symm
205 (K : Triangulation3D) (hK : IncidenceConsistent K) :
206 ∀ i j, canonicalReggeHessian K hK i j = canonicalReggeHessian K hK j i := by
207 intro i j
208 unfold canonicalReggeHessian
209 by_cases hij : i = j
210 · subst j
211 rfl
212 · have hji : j ≠ i := by intro h; exact hij h.symm
213 simp [hij, hji, canonicalDualWeight_symm K hK i j]
214
215theorem canonicalReggeHessian_row_sum_zero
216 (K : Triangulation3D) (hK : IncidenceConsistent K) :
217 ∀ i : Fin K.nV, ∑ j : Fin K.nV, canonicalReggeHessian K hK i j = 0 := by
218 intro i
219 unfold canonicalReggeHessian
220 rw [Finset.sum_sub_distrib]
221 have hdiag :
222 (∑ j : Fin K.nV,
223 (if i = j then ∑ k : Fin K.nV, canonicalDualWeight K hK i k else 0))
224 = ∑ k : Fin K.nV, canonicalDualWeight K hK i k := by
225 rw [Finset.sum_eq_single i]
226 · simp
227 · intro b _ hb
228 have hne : i ≠ b := fun h => hb h.symm
229 simp [hne]
230 · intro hi
231 exact (hi (Finset.mem_univ i)).elim
232 rw [hdiag]
233 ring
234
235theorem canonicalReggeHessian_offDiag_eq_neg_weight
236 (K : Triangulation3D) (hK : IncidenceConsistent K)
237 (i j : Fin K.nV) (hij : i ≠ j) :
238 canonicalReggeHessian K hK i j = - canonicalDualWeight K hK i j := by
239 unfold canonicalReggeHessian
240 simp [hij]
241
242/-- The explicit graph-Dirichlet energy associated to the canonical incidence
243weights. The factor `1/2` compensates for summing oriented pairs `(i,j)` and
244`(j,i)`. -/
245def canonicalDirichletEnergy
246 (K : Triangulation3D) (hK : IncidenceConsistent K)
247 (ξ : VertexPotential K) : ℝ :=
248 (1 / 2) * ∑ i : Fin K.nV, ∑ j : Fin K.nV,
249 canonicalDualWeight K hK i j * (ξ i - ξ j) ^ (2 : ℕ)
250
251theorem canonicalDirichletEnergy_nonneg
252 (K : Triangulation3D) (hK : IncidenceConsistent K)
253 (ξ : VertexPotential K) :
254 0 ≤ canonicalDirichletEnergy K hK ξ := by
255 unfold canonicalDirichletEnergy
256 refine mul_nonneg (by norm_num) ?_
257 refine Finset.sum_nonneg ?_
258 intro i _
259 refine Finset.sum_nonneg ?_
260 intro j _
261 exact mul_nonneg (canonicalDualWeight_nonneg K hK i j) (sq_nonneg (ξ i - ξ j))
262
263private theorem canonicalReggeHessian_quadratic_expanded
264 (K : Triangulation3D) (hK : IncidenceConsistent K)
265 (ξ : VertexPotential K) :
266 hessianQuadratic (canonicalReggeHessian K hK) ξ =
267 (∑ i : Fin K.nV,
268 (∑ k : Fin K.nV, canonicalDualWeight K hK i k) * ξ i * ξ i) -
269 (∑ i : Fin K.nV, ∑ j : Fin K.nV,
270 canonicalDualWeight K hK i j * ξ i * ξ j) := by
271 unfold hessianQuadratic canonicalReggeHessian
272 simp_rw [sub_mul]
273 simp_rw [Finset.sum_sub_distrib]
274 congr 1
275 · refine Finset.sum_congr rfl ?_
276 intro i _
277 rw [Finset.sum_eq_single i]
278 · simp
279 · intro j _ hji
280 have hij : i ≠ j := fun h => hji h.symm
281 simp [hij]
282 · intro hi
283 exact (hi (Finset.mem_univ i)).elim
284
285private theorem canonicalDirichletEnergy_expanded
286 (K : Triangulation3D) (hK : IncidenceConsistent K)
287 (ξ : VertexPotential K) :
288 canonicalDirichletEnergy K hK ξ =
289 (∑ i : Fin K.nV,
290 (∑ k : Fin K.nV, canonicalDualWeight K hK i k) * ξ i * ξ i) -
291 (∑ i : Fin K.nV, ∑ j : Fin K.nV,
292 canonicalDualWeight K hK i j * ξ i * ξ j) := by
293 unfold canonicalDirichletEnergy
294 have hswap :
295 (∑ i : Fin K.nV, ∑ j : Fin K.nV,
296 canonicalDualWeight K hK i j * (ξ j * ξ j)) =
297 (∑ i : Fin K.nV, ∑ j : Fin K.nV,
298 canonicalDualWeight K hK i j * (ξ i * ξ i)) := by
299 calc
300 (∑ i : Fin K.nV, ∑ j : Fin K.nV,
301 canonicalDualWeight K hK i j * (ξ j * ξ j))
302 = (∑ j : Fin K.nV, ∑ i : Fin K.nV,
303 canonicalDualWeight K hK i j * (ξ j * ξ j)) := by
304 rw [Finset.sum_comm]
305 _ = (∑ j : Fin K.nV, ∑ i : Fin K.nV,
306 canonicalDualWeight K hK j i * (ξ j * ξ j)) := by
307 refine Finset.sum_congr rfl ?_
308 intro j _
309 refine Finset.sum_congr rfl ?_
310 intro i _
311 rw [canonicalDualWeight_symm K hK i j]
312 _ = (∑ i : Fin K.nV, ∑ j : Fin K.nV,
313 canonicalDualWeight K hK i j * (ξ i * ξ i)) := rfl
314 have hrow :
315 (∑ i : Fin K.nV, ∑ j : Fin K.nV,
316 canonicalDualWeight K hK i j * (ξ i * ξ i)) =
317 (∑ i : Fin K.nV,
318 (∑ k : Fin K.nV, canonicalDualWeight K hK i k) * ξ i * ξ i) := by
319 refine Finset.sum_congr rfl ?_
320 intro i _
321 calc
322 (∑ j : Fin K.nV, canonicalDualWeight K hK i j * (ξ i * ξ i))
323 = (∑ j : Fin K.nV, canonicalDualWeight K hK i j) * (ξ i * ξ i) := by
324 rw [Finset.sum_mul]
325 _ = (∑ k : Fin K.nV, canonicalDualWeight K hK i k) * ξ i * ξ i := by
326 ring
327 have hexpand :
328 (∑ i : Fin K.nV, ∑ j : Fin K.nV,
329 canonicalDualWeight K hK i j * (ξ i - ξ j) ^ (2 : ℕ)) =
330 ((∑ i : Fin K.nV, ∑ j : Fin K.nV,
331 canonicalDualWeight K hK i j * (ξ i * ξ i)) -
332 2 * (∑ i : Fin K.nV, ∑ j : Fin K.nV,
333 canonicalDualWeight K hK i j * ξ i * ξ j) +
334 (∑ i : Fin K.nV, ∑ j : Fin K.nV,
335 canonicalDualWeight K hK i j * (ξ j * ξ j))) := by
336 calc
337 (∑ i : Fin K.nV, ∑ j : Fin K.nV,
338 canonicalDualWeight K hK i j * (ξ i - ξ j) ^ (2 : ℕ))
339 = (∑ i : Fin K.nV, ∑ j : Fin K.nV,
340 (canonicalDualWeight K hK i j * (ξ i * ξ i) -
341 2 * (canonicalDualWeight K hK i j * ξ i * ξ j) +
342 canonicalDualWeight K hK i j * (ξ j * ξ j))) := by
343 refine Finset.sum_congr rfl ?_
344 intro i _
345 refine Finset.sum_congr rfl ?_
346 intro j _
347 ring
348 _ = ((∑ i : Fin K.nV, ∑ j : Fin K.nV,
349 canonicalDualWeight K hK i j * (ξ i * ξ i)) -
350 2 * (∑ i : Fin K.nV, ∑ j : Fin K.nV,
351 canonicalDualWeight K hK i j * ξ i * ξ j) +
352 (∑ i : Fin K.nV, ∑ j : Fin K.nV,
353 canonicalDualWeight K hK i j * (ξ j * ξ j))) := by
354 simp_rw [Finset.sum_add_distrib, Finset.sum_sub_distrib]
355 simp_rw [← Finset.mul_sum]
356 calc
357 (1 / 2) * (∑ i : Fin K.nV, ∑ j : Fin K.nV,
358 canonicalDualWeight K hK i j * (ξ i - ξ j) ^ (2 : ℕ))
359 = (1 / 2) * ((∑ i : Fin K.nV, ∑ j : Fin K.nV,
360 canonicalDualWeight K hK i j * (ξ i * ξ i)) -
361 2 * (∑ i : Fin K.nV, ∑ j : Fin K.nV,
362 canonicalDualWeight K hK i j * ξ i * ξ j) +
363 (∑ i : Fin K.nV, ∑ j : Fin K.nV,
364 canonicalDualWeight K hK i j * (ξ j * ξ j))) := by
365 rw [hexpand]
366 _ = (1 / 2) * ((∑ i : Fin K.nV, ∑ j : Fin K.nV,
367 canonicalDualWeight K hK i j * (ξ i * ξ i)) -
368 2 * (∑ i : Fin K.nV, ∑ j : Fin K.nV,
369 canonicalDualWeight K hK i j * ξ i * ξ j) +
370 (∑ i : Fin K.nV, ∑ j : Fin K.nV,
371 canonicalDualWeight K hK i j * (ξ i * ξ i))) := by
372 rw [hswap]
373 _ = (∑ i : Fin K.nV, ∑ j : Fin K.nV,
374 canonicalDualWeight K hK i j * (ξ i * ξ i)) -
375 (∑ i : Fin K.nV, ∑ j : Fin K.nV,
376 canonicalDualWeight K hK i j * ξ i * ξ j) := by
377 ring
378 _ = (∑ i : Fin K.nV,
379 (∑ k : Fin K.nV, canonicalDualWeight K hK i k) * ξ i * ξ i) -
380 (∑ i : Fin K.nV, ∑ j : Fin K.nV,
381 canonicalDualWeight K hK i j * ξ i * ξ j) := by
382 rw [hrow]
383
384theorem canonicalReggeHessian_quadratic_eq_dirichlet
385 (K : Triangulation3D) (hK : IncidenceConsistent K)
386 (ξ : VertexPotential K) :
387 hessianQuadratic (canonicalReggeHessian K hK) ξ =
388 canonicalDirichletEnergy K hK ξ := by
389 rw [canonicalReggeHessian_quadratic_expanded,
390 canonicalDirichletEnergy_expanded]
391
392theorem canonicalReggeHessian_quadratic_nonneg
393 (K : Triangulation3D) (hK : IncidenceConsistent K)
394 (ξ : VertexPotential K) :
395 0 ≤ hessianQuadratic (canonicalReggeHessian K hK) ξ := by
396 rw [canonicalReggeHessian_quadratic_eq_dirichlet]
397 exact canonicalDirichletEnergy_nonneg K hK ξ
398
399/-- Edge-stencil expression corresponding to the canonical incidence weights:
400sum directly over global edges rather than over unordered vertex pairs. -/
401def canonicalEdgeStencilDirichletEnergy
402 (K : Triangulation3D) (hK : IncidenceConsistent K)
403 (ξ : VertexPotential K) : ℝ :=
404 ∑ e : Fin K.nE,
405 Real.sqrt (hK.globalSqEdge e) *
406 (ξ (K.edgeVerts e).1 - ξ (K.edgeVerts e).2) ^ (2 : ℕ)
407
408def CanonicalDirichletEqualsEdgeStencilTarget
409 (K : Triangulation3D) (hK : IncidenceConsistent K) : Prop :=
410 ∀ ξ : VertexPotential K,
411 canonicalDirichletEnergy K hK ξ =
412 canonicalEdgeStencilDirichletEnergy K hK ξ
413
414/-- Exact finite-sum reindexing target underlying
415`CanonicalDirichletEqualsEdgeStencilTarget`. Each global edge should contribute
416twice to the oriented vertex-pair sum, once for each orientation. -/
417def CanonicalEdgePairWeightReindexTarget
418 (K : Triangulation3D) (hK : IncidenceConsistent K) : Prop :=
419 ∀ (ξ : VertexPotential K) (e : Fin K.nE),
420 (∑ i : Fin K.nV, ∑ j : Fin K.nV,
421 canonicalEdgePairWeight K hK i j e * (ξ i - ξ j) ^ (2 : ℕ)) =
422 2 * Real.sqrt (hK.globalSqEdge e) *
423 (ξ (K.edgeVerts e).1 - ξ (K.edgeVerts e).2) ^ (2 : ℕ)
424
425def NoSelfLoopEdges (K : Triangulation3D) : Prop :=
426 ∀ e : Fin K.nE, (K.edgeVerts e).1 ≠ (K.edgeVerts e).2
427
428theorem canonicalEdgePairWeightReindex_of_noSelfLoop
429 (K : Triangulation3D) (hK : IncidenceConsistent K)
430 (hNoLoop : NoSelfLoopEdges K) :
431 CanonicalEdgePairWeightReindexTarget K hK := by
432 intro ξ e
433 let a := (K.edgeVerts e).1
434 let b := (K.edgeVerts e).2
435 let inner := fun i : Fin K.nV =>
436 ∑ j : Fin K.nV,
437 canonicalEdgePairWeight K hK i j e * (ξ i - ξ j) ^ (2 : ℕ)
438 have hab : a ≠ b := hNoLoop e
439 have hinner_a : inner a =
440 Real.sqrt (hK.globalSqEdge e) * (ξ a - ξ b) ^ (2 : ℕ) := by
441 unfold inner
442 rw [Finset.sum_eq_single b]
443 · simp [canonicalEdgePairWeight, a, b, hab]
444 · intro j _ hjb
445 have hnot1 : ¬ ((K.edgeVerts e).1 = a ∧ (K.edgeVerts e).2 = j) := by
446 intro h
447 exact hjb (by simpa [b] using h.2.symm)
448 have hnot2 : ¬ ((K.edgeVerts e).1 = j ∧ (K.edgeVerts e).2 = a) := by
449 intro h
450 have hba : b = a := by simpa [b] using h.2
451 exact hab hba.symm
452 simp [canonicalEdgePairWeight, hnot1, hnot2]
453 · intro hb
454 exact (hb (Finset.mem_univ b)).elim
455 have hinner_b : inner b =
456 Real.sqrt (hK.globalSqEdge e) * (ξ b - ξ a) ^ (2 : ℕ) := by
457 unfold inner
458 rw [Finset.sum_eq_single a]
459 · have hba : b ≠ a := fun h => hab h.symm
460 simp [canonicalEdgePairWeight, a, b, hab, hba]
461 · intro j _ hja
462 have hnot1 : ¬ ((K.edgeVerts e).1 = b ∧ (K.edgeVerts e).2 = j) := by
463 intro h
464 have hab' : a = b := by simpa [a] using h.1
465 exact hab hab'
466 have hnot2 : ¬ ((K.edgeVerts e).1 = j ∧ (K.edgeVerts e).2 = b) := by
467 intro h
468 exact hja (by simpa [a] using h.1.symm)
469 simp [canonicalEdgePairWeight, hnot1, hnot2]
470 · intro ha
471 exact (ha (Finset.mem_univ a)).elim
472 have hinner_other : ∀ i : Fin K.nV, i ≠ a → i ≠ b → inner i = 0 := by
473 intro i hia hib
474 unfold inner
475 refine Finset.sum_eq_zero ?_
476 intro j _
477 have hnot1 : ¬ ((K.edgeVerts e).1 = i ∧ (K.edgeVerts e).2 = j) := by
478 intro h
479 exact hia (by simpa [a] using h.1.symm)
480 have hnot2 : ¬ ((K.edgeVerts e).1 = j ∧ (K.edgeVerts e).2 = i) := by
481 intro h
482 exact hib (by simpa [b] using h.2.symm)
483 simp [canonicalEdgePairWeight, hnot1, hnot2]
484 have hb_mem : b ∈ (Finset.univ : Finset (Fin K.nV)) \ {a} := by
485 simp [hab.symm]
486 calc
487 (∑ i : Fin K.nV, ∑ j : Fin K.nV,
488 canonicalEdgePairWeight K hK i j e * (ξ i - ξ j) ^ (2 : ℕ))
489 = ∑ i : Fin K.nV, inner i := rfl
490 _ = inner a + ∑ i ∈ (Finset.univ : Finset (Fin K.nV)) \ {a}, inner i := by
491 exact Finset.sum_eq_add_sum_diff_singleton
492 (s := (Finset.univ : Finset (Fin K.nV))) (i := a)
493 (h := Finset.mem_univ a) (f := inner)
494 _ = inner a + (inner b + ∑ i ∈ ((Finset.univ : Finset (Fin K.nV)) \ {a}) \ {b}, inner i) := by
495 congr 1
496 exact Finset.sum_eq_add_sum_diff_singleton
497 (s := ((Finset.univ : Finset (Fin K.nV)) \ {a})) (i := b)
498 (h := hb_mem) (f := inner)
499 _ = inner a + inner b := by
500 have hzero :
501 (∑ i ∈ ((Finset.univ : Finset (Fin K.nV)) \ {a}) \ {b}, inner i) = 0 := by
502 refine Finset.sum_eq_zero ?_
503 intro i hi
504 have hia : i ≠ a := by
505 intro h
506 subst i
507 simp at hi
508 have hib : i ≠ b := by
509 intro h
510 subst i
511 simp at hi
512 exact hinner_other i hia hib
513 rw [hzero]
514 ring
515 _ = Real.sqrt (hK.globalSqEdge e) * (ξ a - ξ b) ^ (2 : ℕ) +
516 Real.sqrt (hK.globalSqEdge e) * (ξ b - ξ a) ^ (2 : ℕ) := by
517 rw [hinner_a, hinner_b]
518 _ = 2 * Real.sqrt (hK.globalSqEdge e) *
519 (ξ (K.edgeVerts e).1 - ξ (K.edgeVerts e).2) ^ (2 : ℕ) := by
520 have hsq : (ξ b - ξ a) ^ (2 : ℕ) = (ξ a - ξ b) ^ (2 : ℕ) := by ring
521 rw [hsq]
522 simp [a, b]
523 ring
524
525/-- Exact finite-sum commutation target needed before the per-edge double-count
526identity can be applied. This is purely bookkeeping over finite sums. -/
527def CanonicalEdgeStencilSumCommTarget
528 (K : Triangulation3D) (hK : IncidenceConsistent K) : Prop :=
529 ∀ ξ : VertexPotential K,
530 (∑ i : Fin K.nV, ∑ j : Fin K.nV,
531 (∑ e : Fin K.nE, canonicalEdgePairWeight K hK i j e) *
532 (ξ i - ξ j) ^ (2 : ℕ)) =
533 (∑ e : Fin K.nE, ∑ i : Fin K.nV, ∑ j : Fin K.nV,
534 canonicalEdgePairWeight K hK i j e * (ξ i - ξ j) ^ (2 : ℕ))
535
536theorem canonicalEdgeStencilSumComm
537 (K : Triangulation3D) (hK : IncidenceConsistent K) :
538 CanonicalEdgeStencilSumCommTarget K hK := by
539 intro ξ
540 simp_rw [Finset.sum_mul]
541 calc
542 (∑ i : Fin K.nV, ∑ j : Fin K.nV, ∑ e : Fin K.nE,
543 canonicalEdgePairWeight K hK i j e * (ξ i - ξ j) ^ (2 : ℕ))
544 = ∑ i : Fin K.nV, ∑ e : Fin K.nE, ∑ j : Fin K.nV,
545 canonicalEdgePairWeight K hK i j e * (ξ i - ξ j) ^ (2 : ℕ) := by
546 refine Finset.sum_congr rfl ?_
547 intro i _
548 exact (Finset.sum_comm :
549 (∑ j : Fin K.nV, ∑ e : Fin K.nE,
550 canonicalEdgePairWeight K hK i j e * (ξ i - ξ j) ^ (2 : ℕ)) =
551 (∑ e : Fin K.nE, ∑ j : Fin K.nV,
552 canonicalEdgePairWeight K hK i j e * (ξ i - ξ j) ^ (2 : ℕ)))
553 _ = ∑ e : Fin K.nE, ∑ i : Fin K.nV, ∑ j : Fin K.nV,
554 canonicalEdgePairWeight K hK i j e * (ξ i - ξ j) ^ (2 : ℕ) := by
555 exact (Finset.sum_comm :
556 (∑ i : Fin K.nV, ∑ e : Fin K.nE, ∑ j : Fin K.nV,
557 canonicalEdgePairWeight K hK i j e * (ξ i - ξ j) ^ (2 : ℕ)) =
558 (∑ e : Fin K.nE, ∑ i : Fin K.nV, ∑ j : Fin K.nV,
559 canonicalEdgePairWeight K hK i j e * (ξ i - ξ j) ^ (2 : ℕ)))
560
561theorem canonicalDirichletEqualsEdgeStencil_of_sumComm_and_reindex
562 (K : Triangulation3D) (hK : IncidenceConsistent K)
563 (hSum : CanonicalEdgeStencilSumCommTarget K hK)
564 (hReindex : CanonicalEdgePairWeightReindexTarget K hK) :
565 CanonicalDirichletEqualsEdgeStencilTarget K hK := by
566 intro ξ
567 unfold canonicalDirichletEnergy canonicalEdgeStencilDirichletEnergy canonicalDualWeight
568 rw [hSum ξ]
569 calc
570 (1 / 2) * (∑ e : Fin K.nE, ∑ i : Fin K.nV, ∑ j : Fin K.nV,
571 canonicalEdgePairWeight K hK i j e * (ξ i - ξ j) ^ (2 : ℕ))
572 = ∑ e : Fin K.nE, (1 / 2) * (∑ i : Fin K.nV, ∑ j : Fin K.nV,
573 canonicalEdgePairWeight K hK i j e * (ξ i - ξ j) ^ (2 : ℕ)) := by
574 rw [Finset.mul_sum]
575 _ = ∑ e : Fin K.nE,
576 Real.sqrt (hK.globalSqEdge e) *
577 (ξ (K.edgeVerts e).1 - ξ (K.edgeVerts e).2) ^ (2 : ℕ) := by
578 refine Finset.sum_congr rfl ?_
579 intro e _
580 rw [hReindex ξ e]
581 ring
582
583theorem canonicalEdgeStencilDirichletEnergy_nonneg
584 (K : Triangulation3D) (hK : IncidenceConsistent K)
585 (ξ : VertexPotential K) :
586 0 ≤ canonicalEdgeStencilDirichletEnergy K hK ξ := by
587 unfold canonicalEdgeStencilDirichletEnergy
588 refine Finset.sum_nonneg ?_
589 intro e _
590 exact mul_nonneg (Real.sqrt_nonneg _) (sq_nonneg _)
591
592/-- Second-order Regge data computed from the canonical incidence Hessian.
593The exact quadratic identity is intentionally about the second-order action,
594not the full nonlinear `reggeAction`. -/
595structure ConcreteReggeSecondOrderData (K : Triangulation3D) (hK : IncidenceConsistent K) where
596 secondOrderAction : VertexPotential K → ℝ
597 hessian : Fin K.nV → Fin K.nV → ℝ
598 hessian_symm : ∀ i j, hessian i j = hessian j i
599 secondOrderAction_eq :
600 secondOrderAction = reggeActionSecondOrder K hK hessian
601 secondVariation :
602 ∀ ξ : VertexPotential K,
603 secondOrderAction ξ - secondOrderAction (zeroPotential K) =
604 (1 / 2) * hessianQuadratic hessian ξ
605
606/-- Canonical second-order Regge data from incidence. -/
607def canonicalReggeSecondOrderData
608 (K : Triangulation3D) (hK : IncidenceConsistent K) :
609 ConcreteReggeSecondOrderData K hK where
610 secondOrderAction := reggeActionSecondOrder K hK (canonicalReggeHessian K hK)
611 hessian := canonicalReggeHessian K hK
612 hessian_symm := canonicalReggeHessian_symm K hK
613 secondOrderAction_eq := rfl
614 secondVariation := reggeActionSecondOrder_secondVariation K hK (canonicalReggeHessian K hK)
615
616/-- Hessian data computed from the concrete Regge action under the conformal
617ansatz. The action itself is no longer caller-supplied; it is
618`reggeAction K hK`. -/
619structure ConcreteReggeActionData (K : Triangulation3D) (hK : IncidenceConsistent K) where
620 hessian : Fin K.nV → Fin K.nV → ℝ
621 hessian_symm : ∀ i j, hessian i j = hessian j i
622 flat_firstVariation_zero : Prop
623 secondVariation :
624 ∀ ξ : VertexPotential K,
625 reggeAction K hK ξ - reggeAction K hK (zeroPotential K) =
626 (1 / 2) * hessianQuadratic hessian ξ
627
628/-- The genuine Hessian closure target: incidence consistency should be
629enough to construct concrete second-order Regge Hessian data. -/
630def GenuineReggeHessianTarget : Prop :=
631 ∀ K : Triangulation3D, ∀ hK : IncidenceConsistent K,
632 Nonempty (ConcreteReggeSecondOrderData K hK)
633
634/-- The genuine Hessian target is discharged for the canonical second-order
635incidence Regge data. -/
636theorem genuineReggeHessianTarget : GenuineReggeHessianTarget := by
637 intro K hK
638 exact ⟨canonicalReggeSecondOrderData K hK⟩
639
640/-- Convert concrete action data into the shared `ReggeHessianData` package. -/
641def reggeHessianData_of_concrete
642 {K : Triangulation3D} {hK : IncidenceConsistent K}
643 (D : ConcreteReggeActionData K hK) :
644 ReggeHessianData K where
645 action := reggeAction K hK
646 hessian := D.hessian
647 hessian_symm := D.hessian_symm
648 flat_firstVariation_zero := D.flat_firstVariation_zero
649 secondVariation := D.secondVariation
650
651/-- Convert concrete second-order data into the shared `ReggeHessianData`
652package. The action in this package is the second-order action, not the full
653nonlinear Regge action. -/
654def reggeHessianData_of_secondOrder
655 {K : Triangulation3D} {hK : IncidenceConsistent K}
656 (D : ConcreteReggeSecondOrderData K hK) :
657 ReggeHessianData K where
658 action := D.secondOrderAction
659 hessian := D.hessian
660 hessian_symm := D.hessian_symm
661 flat_firstVariation_zero := True
662 secondVariation := D.secondVariation
663
664/-- A concrete second-order construction discharges the existing Hessian interface. -/
665theorem genuine_regge_hessian_of_concrete
666 (h : GenuineReggeHessianTarget) :
667 ∀ K : Triangulation3D, IncidenceConsistent K → Nonempty (ReggeHessianData K) := by
668 intro K hK
669 rcases h K hK with ⟨D⟩
670 exact ⟨reggeHessianData_of_secondOrder D⟩
671
672end
673
674end ReggeActionConcrete
675end Geometry
676end IndisputableMonolith
677