IndisputableMonolith.Geometry.ReggeActionFirstVariation
IndisputableMonolith/Geometry/ReggeActionFirstVariation.lean · 1203 lines · 65 declarations
show as:
view math explainer →
1import Mathlib
2import IndisputableMonolith.Geometry.ReggeActionSmoothness
3import IndisputableMonolith.Geometry.SchlaefliTetrahedronProof
4import IndisputableMonolith.Geometry.SchlaefliTriangulation3D
5
6/-!
7# First Variation of the Nonlinear Regge Action
8
9The target theorem is the vanishing of the first variation of the full
10nonlinear Regge action at the flat conformal potential. The geometric proof
11is Schläfli cancellation plus zero deficit. This module records the exact
12analytic statement and the named input needed until the full derivative
13calculation is expanded from the closed-form local Schläfli identities.
14-/
15
16namespace IndisputableMonolith
17namespace Geometry
18namespace ReggeActionFirstVariation
19
20open ReggeTriangulation3D
21open ReggeHessian3D
22open Triangulation3DConsistency
23open ReggeActionConcrete
24open ReggeActionSmoothness
25open SchlaefliTetrahedronProof
26open SchlaefliTriangulation3D
27open DihedralCayleyMenger
28
29noncomputable section
30
31/-- The line through the flat potential in direction `η`. This local copy
32keeps the first-variation module independent of the second-variation module. -/
33def linePotential (K : Triangulation3D) (η : VertexPotential K) (t : ℝ) :
34 VertexPotential K :=
35 fun i => t * η i
36
37theorem linePotential_zero
38 (K : Triangulation3D) (η : VertexPotential K) :
39 linePotential K η 0 = zeroPotential K := by
40 funext i
41 simp [linePotential, zeroPotential]
42
43/-- Every vector in `Fin 6 → ℝ` is the sum of its coordinate basis pieces,
44and a continuous linear functional is determined by those six values. -/
45theorem continuousLinearMap_apply_eq_sum_single
46 (L : (Fin 6 → ℝ) →L[ℝ] ℝ) (v : Fin 6 → ℝ) :
47 L v = ∑ k : Fin 6, v k * L (Pi.single (M := fun _ : Fin 6 => ℝ) k (1 : ℝ)) := by
48 have hv : (∑ k : Fin 6, Pi.single (M := fun _ : Fin 6 => ℝ) k (v k)) = v :=
49 Finset.univ_sum_single v
50 calc
51 L v = L (∑ k : Fin 6, Pi.single (M := fun _ : Fin 6 => ℝ) k (v k)) := by rw [hv]
52 _ = ∑ k : Fin 6, L (Pi.single (M := fun _ : Fin 6 => ℝ) k (v k)) := by
53 rw [map_sum]
54 _ = ∑ k : Fin 6, v k * L (Pi.single (M := fun _ : Fin 6 => ℝ) k (1 : ℝ)) := by
55 refine Finset.sum_congr rfl ?_
56 intro k _
57 have hsingle :
58 Pi.single (M := fun _ : Fin 6 => ℝ) k (v k) =
59 v k • Pi.single (M := fun _ : Fin 6 => ℝ) k (1 : ℝ) := by
60 funext i
61 by_cases hik : i = k
62 · subst i
63 simp [Pi.single_eq_same]
64 · simp [hik]
65 rw [hsingle, map_smul]
66 simp [smul_eq_mul]
67
68theorem functionUpdate_hasDerivAt_single
69 (a : Fin 6 → ℝ) (k : Fin 6) :
70 HasDerivAt (fun t : ℝ => Function.update a k t)
71 (Pi.single (M := fun _ : Fin 6 => ℝ) k (1 : ℝ)) (a k) := by
72 rw [hasDerivAt_pi]
73 intro i
74 by_cases hik : i = k
75 · subst i
76 simpa [Function.update] using (hasDerivAt_id (a k))
77 · have hconst : (fun t : ℝ => Function.update a k t i) = fun _t : ℝ => a i := by
78 funext t
79 simp [Function.update, hik]
80 rw [hconst]
81 simpa [Pi.single_eq_of_ne hik] using hasDerivAt_const (a k) (a i)
82
83/-- Directional derivative of a local conformal squared-edge coordinate at the
84flat potential. -/
85def conformalLocalSqEdgeDirectionalDeriv
86 (K : Triangulation3D) (η : VertexPotential K)
87 (τ : Fin K.nT) (f : Fin 6) : ℝ :=
88 let uv := ReggeRigorousFoundation.edgeVertices f
89 (K.tet τ).sqEdge f * (η (K.tetVerts τ uv.1) + η (K.tetVerts τ uv.2))
90
91theorem conformalLocalSqEdge_hasDerivAt_line_zero
92 (K : Triangulation3D) (η : VertexPotential K)
93 (τ : Fin K.nT) (f : Fin 6) :
94 HasDerivAt
95 (fun t : ℝ => conformalLocalSqEdge K (linePotential K η t) τ f)
96 (conformalLocalSqEdgeDirectionalDeriv K η τ f) 0 := by
97 unfold conformalLocalSqEdge conformalLocalSqEdgeDirectionalDeriv linePotential
98 let uv := ReggeRigorousFoundation.edgeVertices f
99 have hlin : HasDerivAt
100 (fun t : ℝ => t * η (K.tetVerts τ uv.1) + t * η (K.tetVerts τ uv.2))
101 (η (K.tetVerts τ uv.1) + η (K.tetVerts τ uv.2)) 0 := by
102 have h1 : HasDerivAt
103 (fun t : ℝ => t * η (K.tetVerts τ uv.1))
104 (η (K.tetVerts τ uv.1)) 0 :=
105 by simpa using (hasDerivAt_id 0).mul_const (η (K.tetVerts τ uv.1))
106 have h2 : HasDerivAt
107 (fun t : ℝ => t * η (K.tetVerts τ uv.2))
108 (η (K.tetVerts τ uv.2)) 0 :=
109 by simpa using (hasDerivAt_id 0).mul_const (η (K.tetVerts τ uv.2))
110 exact h1.add h2
111 have hexp : HasDerivAt
112 (fun t : ℝ =>
113 Real.exp (t * η (K.tetVerts τ uv.1) + t * η (K.tetVerts τ uv.2)))
114 (η (K.tetVerts τ uv.1) + η (K.tetVerts τ uv.2)) 0 := by
115 have h := (Real.hasDerivAt_exp
116 (0 * η (K.tetVerts τ uv.1) + 0 * η (K.tetVerts τ uv.2))).comp 0 hlin
117 simpa [Real.exp_zero] using h
118 simpa [uv, Real.exp_zero, mul_comm, mul_left_comm, mul_assoc] using
119 hexp.const_mul ((K.tet τ).sqEdge f)
120
121theorem conformalTetSqEdges_hasDerivAt_line_zero
122 (K : Triangulation3D) (η : VertexPotential K) (τ : Fin K.nT) :
123 HasDerivAt
124 (fun t : ℝ => conformalTetSqEdges K (linePotential K η t) τ)
125 (fun f : Fin 6 => conformalLocalSqEdgeDirectionalDeriv K η τ f) 0 := by
126 rw [hasDerivAt_pi]
127 intro f
128 exact conformalLocalSqEdge_hasDerivAt_line_zero K η τ f
129
130theorem dihedralDenom3_contDiffAt_nonDegenerate
131 (T : ReggeRigorousFoundation.NonDegenerateTet) (f : Fin 6) (n : ℕ∞) :
132 ContDiffAt ℝ n (fun a : CayleyMengerPolynomial.SqEdges => dihedralDenom3 a f)
133 T.sqEdge := by
134 unfold dihedralDenom3
135 let p := (oppositeCMVertices f).1
136 let q := (oppositeCMVertices f).2
137 have hpp : ContDiffAt ℝ n
138 (fun a : CayleyMengerPolynomial.SqEdges => CayleyMengerMatrix.cmCofactor3 a p p)
139 T.sqEdge :=
140 (CayleyMengerMatrix.cmCofactor3_contDiff n p p).contDiffAt
141 have hqq : ContDiffAt ℝ n
142 (fun a : CayleyMengerPolynomial.SqEdges => CayleyMengerMatrix.cmCofactor3 a q q)
143 T.sqEdge :=
144 (CayleyMengerMatrix.cmCofactor3_contDiff n q q).contDiffAt
145 have hprod : ContDiffAt ℝ n (fun a : CayleyMengerPolynomial.SqEdges =>
146 CayleyMengerMatrix.cmCofactor3 a p p * CayleyMengerMatrix.cmCofactor3 a q q)
147 T.sqEdge :=
148 hpp.mul hqq
149 have hden : dihedralDenom3 T.sqEdge f ≠ 0 := by
150 rw [CofactorDerivatives.dihedralDenom3_eq_poly]
151 exact CofactorDerivatives.dihedralDenom3Poly_ne_zero_of_nonDegenerate T f
152 have hprod_ne :
153 CayleyMengerMatrix.cmCofactor3 T.sqEdge p p *
154 CayleyMengerMatrix.cmCofactor3 T.sqEdge q q ≠ 0 := by
155 intro hzero
156 apply hden
157 simp [dihedralDenom3, p, q, hzero]
158 simpa [p, q] using hprod.sqrt hprod_ne
159
160theorem dihedralCos3Sq_contDiffAt_nonDegenerate
161 (T : ReggeRigorousFoundation.NonDegenerateTet) (f : Fin 6) (n : ℕ∞) :
162 ContDiffAt ℝ n (fun a : CayleyMengerPolynomial.SqEdges => dihedralCos3Sq a f)
163 T.sqEdge := by
164 unfold dihedralCos3Sq
165 let p := (oppositeCMVertices f).1
166 let q := (oppositeCMVertices f).2
167 have hnum : ContDiffAt ℝ n
168 (fun a : CayleyMengerPolynomial.SqEdges => CayleyMengerMatrix.cmCofactor3 a p q)
169 T.sqEdge :=
170 (CayleyMengerMatrix.cmCofactor3_contDiff n p q).contDiffAt
171 have hden := dihedralDenom3_contDiffAt_nonDegenerate T f n
172 have hden_ne : dihedralDenom3 T.sqEdge f ≠ 0 := by
173 rw [CofactorDerivatives.dihedralDenom3_eq_poly]
174 exact CofactorDerivatives.dihedralDenom3Poly_ne_zero_of_nonDegenerate T f
175 simpa [p, q] using hnum.div hden hden_ne
176
177theorem dihedralAngle3Sq_contDiffAt_nonDegenerate
178 (T : ReggeRigorousFoundation.NonDegenerateTet) (f : Fin 6) (n : ℕ∞)
179 (hEndpoint : dihedralCos3Sq T.sqEdge f ≠ -1 ∧ dihedralCos3Sq T.sqEdge f ≠ 1) :
180 ContDiffAt ℝ n
181 (fun a : CayleyMengerPolynomial.SqEdges => DihedralDerivatives.dihedralAngle3Sq a f)
182 T.sqEdge := by
183 unfold DihedralDerivatives.dihedralAngle3Sq
184 have hcos := dihedralCos3Sq_contDiffAt_nonDegenerate T f n
185 have hacos : ContDiffAt ℝ n Real.arccos (dihedralCos3Sq T.sqEdge f) :=
186 Real.contDiffAt_arccos hEndpoint.1 hEndpoint.2
187 simpa [Function.comp_def] using
188 (ContDiffAt.comp (x := T.sqEdge) hacos hcos)
189
190theorem fderiv_dihedralAngle3Sq_apply_single
191 (T : ReggeRigorousFoundation.NonDegenerateTet) (f k : Fin 6)
192 (hEndpoint : dihedralCos3Sq T.sqEdge f ≠ -1 ∧ dihedralCos3Sq T.sqEdge f ≠ 1) :
193 (fderiv ℝ
194 (fun a : CayleyMengerPolynomial.SqEdges => DihedralDerivatives.dihedralAngle3Sq a f)
195 T.sqEdge) (Pi.single (M := fun _ : Fin 6 => ℝ) k (1 : ℝ)) =
196 dihedralClosedDerivSq T f k := by
197 have hAngle : ContDiffAt ℝ 1
198 (fun a : CayleyMengerPolynomial.SqEdges => DihedralDerivatives.dihedralAngle3Sq a f)
199 T.sqEdge :=
200 dihedralAngle3Sq_contDiffAt_nonDegenerate T f 1 hEndpoint
201 have hDiff : DifferentiableAt ℝ
202 (fun a : CayleyMengerPolynomial.SqEdges => DihedralDerivatives.dihedralAngle3Sq a f)
203 T.sqEdge :=
204 hAngle.differentiableAt (by simp)
205 have hF : HasFDerivAt
206 (fun a : CayleyMengerPolynomial.SqEdges => DihedralDerivatives.dihedralAngle3Sq a f)
207 (fderiv ℝ
208 (fun a : CayleyMengerPolynomial.SqEdges => DihedralDerivatives.dihedralAngle3Sq a f)
209 T.sqEdge)
210 T.sqEdge :=
211 hDiff.hasFDerivAt
212 have hbase : Function.update T.sqEdge k (T.sqEdge k) = T.sqEdge := by
213 funext i
214 by_cases hik : i = k <;> simp [Function.update, hik]
215 have hF' : HasFDerivAt
216 (fun a : CayleyMengerPolynomial.SqEdges => DihedralDerivatives.dihedralAngle3Sq a f)
217 (fderiv ℝ
218 (fun a : CayleyMengerPolynomial.SqEdges => DihedralDerivatives.dihedralAngle3Sq a f)
219 T.sqEdge)
220 (Function.update T.sqEdge k (T.sqEdge k)) := by
221 simpa [hbase] using hF
222 have hupdate := functionUpdate_hasDerivAt_single T.sqEdge k
223 have hcomp := HasFDerivAt.comp_hasDerivAt
224 (x := T.sqEdge k)
225 (f := fun t : ℝ => Function.update T.sqEdge k t)
226 (l := fun a : CayleyMengerPolynomial.SqEdges => DihedralDerivatives.dihedralAngle3Sq a f)
227 hF' hupdate
228 let p := (oppositeCMVertices f).1
229 let q := (oppositeCMVertices f).2
230 have hden : dihedralDenom3 T.sqEdge f ≠ 0 := by
231 rw [CofactorDerivatives.dihedralDenom3_eq_poly]
232 exact CofactorDerivatives.dihedralDenom3Poly_ne_zero_of_nonDegenerate T f
233 have hprod_ne :
234 CayleyMengerMatrix.cmCofactor3 T.sqEdge p p *
235 CayleyMengerMatrix.cmCofactor3 T.sqEdge q q ≠ 0 := by
236 intro hzero
237 apply hden
238 simp [dihedralDenom3, p, q, hzero]
239 have hcoord :=
240 DihedralDerivatives.hasDerivAt_dihedralAngle3Sq_explicit
241 T.sqEdge f k hprod_ne hden hEndpoint.1 hEndpoint.2
242 have hunique := hcomp.unique hcoord
243 simpa [dihedralClosedDerivSq, Function.comp_def] using hunique
244
245/-- Directional derivative of the conformal hinge length at the flat
246potential. -/
247def hingeMeasureDirectionalDeriv
248 (K : Triangulation3D) (hK : IncidenceConsistent K)
249 (η : VertexPotential K) (e : Fin K.nE) : ℝ :=
250 let uv := K.edgeVerts e
251 Real.sqrt (hK.globalSqEdge e) * ((η uv.1 + η uv.2) / 2)
252
253theorem hingeMeasureUnderConformal_hasDerivAt_line_zero
254 (K : Triangulation3D) (hK : IncidenceConsistent K)
255 (η : VertexPotential K) (e : Fin K.nE) :
256 HasDerivAt
257 (fun t : ℝ => hingeMeasureUnderConformal K hK (linePotential K η t) e)
258 (hingeMeasureDirectionalDeriv K hK η e) 0 := by
259 unfold hingeMeasureUnderConformal hingeMeasureDirectionalDeriv linePotential
260 let uv := K.edgeVerts e
261 have hlin : HasDerivAt
262 (fun t : ℝ => (t * η uv.1 + t * η uv.2) / 2)
263 ((η uv.1 + η uv.2) / 2) 0 := by
264 have h1 : HasDerivAt (fun t : ℝ => t * η uv.1) (η uv.1) 0 :=
265 by simpa using (hasDerivAt_id 0).mul_const (η uv.1)
266 have h2 : HasDerivAt (fun t : ℝ => t * η uv.2) (η uv.2) 0 :=
267 by simpa using (hasDerivAt_id 0).mul_const (η uv.2)
268 simpa [add_div] using (h1.add h2).div_const 2
269 have hexp : HasDerivAt
270 (fun t : ℝ => Real.exp ((t * η uv.1 + t * η uv.2) / 2))
271 ((η uv.1 + η uv.2) / 2) 0 := by
272 have h := (Real.hasDerivAt_exp ((0 * η uv.1 + 0 * η uv.2) / 2)).comp 0 hlin
273 simpa [Real.exp_zero] using h
274 simpa [uv, Real.exp_zero, mul_comm, mul_left_comm, mul_assoc] using
275 hexp.const_mul (Real.sqrt (hK.globalSqEdge e))
276
277theorem linePotential_hasDerivAt_zero
278 (K : Triangulation3D) (η : VertexPotential K) :
279 HasDerivAt (fun t : ℝ => linePotential K η t) η 0 := by
280 rw [hasDerivAt_pi]
281 intro i
282 unfold linePotential
283 simpa using (hasDerivAt_id 0).mul_const (η i)
284
285theorem reggeAction_along_line_hasDerivAt_fderiv
286 (K : Triangulation3D) (hK : IncidenceConsistent K)
287 (h_flat : FlatConfiguration K hK) (η : VertexPotential K) :
288 HasDerivAt
289 (fun t : ℝ => reggeAction K hK (linePotential K η t))
290 ((fderiv ℝ (reggeAction K hK) (zeroPotential K)) η) 0 := by
291 have hdiff : DifferentiableAt ℝ (reggeAction K hK) (zeroPotential K) :=
292 h_flat.action_contDiff_at_zero.differentiableAt (by simp)
293 have hF : HasFDerivAt (reggeAction K hK)
294 (fderiv ℝ (reggeAction K hK) (zeroPotential K)) (zeroPotential K) :=
295 hdiff.hasFDerivAt
296 have hF' : HasFDerivAt (reggeAction K hK)
297 (fderiv ℝ (reggeAction K hK) (zeroPotential K)) (linePotential K η 0) := by
298 simpa [linePotential_zero K η] using hF
299 have hline := linePotential_hasDerivAt_zero K η
300 have hcomp := HasFDerivAt.comp_hasDerivAt
301 (x := (0 : ℝ))
302 (f := fun t : ℝ => linePotential K η t)
303 (l := reggeAction K hK)
304 hF' hline
305 simpa [Function.comp_def, linePotential_zero K η] using hcomp
306
307/-- The nonlinear Regge action is critical at the flat potential. -/
308def ReggeActionCriticalAtZero
309 (K : Triangulation3D) (hK : IncidenceConsistent K) : Prop :=
310 fderiv ℝ (reggeAction K hK) (zeroPotential K) = 0
311
312/-- Directional form of criticality, useful while deriving the first
313variation by differentiating along lines. -/
314def ReggeActionDirectionalCriticalAtZero
315 (K : Triangulation3D) (hK : IncidenceConsistent K) : Prop :=
316 ∀ η : VertexPotential K,
317 (fderiv ℝ (reggeAction K hK) (zeroPotential K)) η = 0
318
319theorem reggeActionCriticalAtZero_of_directional
320 (K : Triangulation3D) (hK : IncidenceConsistent K)
321 (hdir : ReggeActionDirectionalCriticalAtZero K hK) :
322 ReggeActionCriticalAtZero K hK := by
323 unfold ReggeActionCriticalAtZero
324 ext η
325 exact hdir η
326
327/-- Explicit first-variation formula in directional form. The hard analytic
328work left in the nonlinear action is to derive this formula by differentiating
329the hinge and dihedral terms and applying global Schläfli to the angle term. -/
330structure ReggeActionFirstVariationFormula
331 (K : Triangulation3D) (hK : IncidenceConsistent K) where
332 firstVariation_formula :
333 ∀ η : VertexPotential K,
334 (fderiv ℝ (reggeAction K hK) (zeroPotential K)) η =
335 ∑ e : Fin K.nE,
336 hingeMeasureDirectionalDeriv K hK η e *
337 deficitAngle K (zeroPotential K) e
338
339/-- Directional first-variation formula along every line through the flat
340potential. This is the form produced directly by one-variable product-rule
341calculations. -/
342structure ReggeActionDirectionalFirstVariationFormula
343 (K : Triangulation3D) (hK : IncidenceConsistent K) where
344 directional_formula :
345 ∀ η : VertexPotential K,
346 HasDerivAt
347 (fun t : ℝ => reggeAction K hK (linePotential K η t))
348 (∑ e : Fin K.nE,
349 hingeMeasureDirectionalDeriv K hK η e *
350 deficitAngle K (zeroPotential K) e) 0
351
352/-- Local dihedral-angle directional derivatives under the conformal ansatz.
353This is the precise local cofactor/arccos derivative target left to prove. -/
354structure LocalDihedralDirectionalDerivativePackage
355 (K : Triangulation3D) where
356 angleDeriv : VertexPotential K → Fin K.nT → Fin 6 → ℝ
357 angle_hasDerivAt :
358 ∀ (η : VertexPotential K) (τ : Fin K.nT) (f : Fin 6),
359 HasDerivAt
360 (fun t : ℝ => tetDihedralAngleUnderConformal K (linePotential K η t) τ f)
361 (angleDeriv η τ f) 0
362
363def localDihedralDirectionalDerivativePackage_of_flat
364 (K : Triangulation3D) (hK : IncidenceConsistent K)
365 (h_flat : FlatConfiguration K hK) :
366 LocalDihedralDirectionalDerivativePackage K where
367 angleDeriv := fun η τ f =>
368 deriv (fun t : ℝ => tetDihedralAngleUnderConformal K (linePotential K η t) τ f) 0
369 angle_hasDerivAt := by
370 intro η τ f
371 have hAngle : ContDiffAt ℝ 1
372 (fun ξ : VertexPotential K => tetDihedralAngleUnderConformal K ξ τ f)
373 (zeroPotential K) :=
374 ReggeActionSmoothness.tetDihedralAngleUnderConformal_contDiffAt_zero
375 K τ f 1 (h_flat.local_arccos_endpoint_free τ f)
376 have hDiffAt : DifferentiableAt ℝ
377 (fun ξ : VertexPotential K => tetDihedralAngleUnderConformal K ξ τ f)
378 (zeroPotential K) :=
379 hAngle.differentiableAt (by simp)
380 have hF : HasFDerivAt
381 (fun ξ : VertexPotential K => tetDihedralAngleUnderConformal K ξ τ f)
382 (fderiv ℝ (fun ξ : VertexPotential K => tetDihedralAngleUnderConformal K ξ τ f)
383 (zeroPotential K))
384 (zeroPotential K) :=
385 hDiffAt.hasFDerivAt
386 have hF' : HasFDerivAt
387 (fun ξ : VertexPotential K => tetDihedralAngleUnderConformal K ξ τ f)
388 (fderiv ℝ (fun ξ : VertexPotential K => tetDihedralAngleUnderConformal K ξ τ f)
389 (zeroPotential K))
390 (linePotential K η 0) := by
391 simpa [linePotential_zero K η] using hF
392 have hline := linePotential_hasDerivAt_zero K η
393 have hcomp := HasFDerivAt.comp_hasDerivAt
394 (x := (0 : ℝ))
395 (f := fun t : ℝ => linePotential K η t)
396 (l := fun ξ : VertexPotential K => tetDihedralAngleUnderConformal K ξ τ f)
397 hF' hline
398 convert hcomp using 1
399 exact hcomp.deriv
400
401/-- Directional derivative of the local edge length `sqrt a_f` induced by a
402vertex-conformal potential direction. -/
403def localEdgeLengthDirectionalDeriv
404 (K : Triangulation3D) (η : VertexPotential K)
405 (τ : Fin K.nT) (f : Fin 6) : ℝ :=
406 let uv := ReggeRigorousFoundation.edgeVertices f
407 Real.sqrt ((K.tet τ).sqEdge f) *
408 ((η (K.tetVerts τ uv.1) + η (K.tetVerts τ uv.2)) / 2)
409
410/-- The angle derivative predicted by the local edge-length chain rule and the
411closed Schläfli derivative data. -/
412def localAngleLengthChainDeriv
413 (K : Triangulation3D) (hK : IncidenceConsistent K)
414 (η : VertexPotential K) (τ : Fin K.nT) (f : Fin 6) : ℝ :=
415 ∑ k : Fin 6,
416 ((triangulationSchlaefliData_of_incidence K hK).tetData τ).dihedralDeriv f k *
417 localEdgeLengthDirectionalDeriv K η τ k
418
419/-- The same local angle derivative written in squared-edge coordinates. -/
420def localAngleSqEdgeChainDeriv
421 (K : Triangulation3D) (η : VertexPotential K)
422 (τ : Fin K.nT) (f : Fin 6) : ℝ :=
423 ∑ k : Fin 6,
424 dihedralClosedDerivSq (K.tet τ) f k *
425 conformalLocalSqEdgeDirectionalDeriv K η τ k
426
427theorem localAngleLengthChainDeriv_eq_sqEdgeChainDeriv
428 (K : Triangulation3D) (hK : IncidenceConsistent K)
429 (η : VertexPotential K) (τ : Fin K.nT) (f : Fin 6) :
430 localAngleLengthChainDeriv K hK η τ f =
431 localAngleSqEdgeChainDeriv K η τ f := by
432 unfold localAngleLengthChainDeriv localAngleSqEdgeChainDeriv
433 refine Finset.sum_congr rfl ?_
434 intro k _
435 have htet :
436 ((triangulationSchlaefliData_of_incidence K hK).tetData τ).dihedralDeriv f k =
437 dihedralClosedDerivLength (K.tet τ) f k := by
438 rfl
439 rw [htet]
440 unfold localEdgeLengthDirectionalDeriv conformalLocalSqEdgeDirectionalDeriv
441 dihedralClosedDerivLength
442 let uv := ReggeRigorousFoundation.edgeVertices k
443 have hsqrt_sq :
444 Real.sqrt ((K.tet τ).sqEdge k) * Real.sqrt ((K.tet τ).sqEdge k) =
445 (K.tet τ).sqEdge k := by
446 rw [← sq]
447 exact Real.sq_sqrt (le_of_lt ((K.tet τ).sqEdge_pos k))
448 have hsqrt_sq_pow :
449 Real.sqrt ((K.tet τ).sqEdge k) ^ 2 = (K.tet τ).sqEdge k := by
450 simpa [pow_two] using hsqrt_sq
451 rw [mul_assoc]
452 ring_nf
453 rw [hsqrt_sq_pow]
454 ring
455
456/-- Local Schläfli cancellation for the conformal length direction on a single
457tetrahedron. This is pure finite-sum algebra plus the already proved local
458Schläfli identity. -/
459theorem local_conformal_schlaefli_cancellation
460 (K : Triangulation3D) (hK : IncidenceConsistent K)
461 (η : VertexPotential K) (τ : Fin K.nT) :
462 (∑ f : Fin 6,
463 Real.sqrt ((K.tet τ).sqEdge f) *
464 localAngleLengthChainDeriv K hK η τ f) = 0 := by
465 unfold localAngleLengthChainDeriv
466 calc
467 (∑ f : Fin 6,
468 Real.sqrt ((K.tet τ).sqEdge f) *
469 (∑ k : Fin 6,
470 ((triangulationSchlaefliData_of_incidence K hK).tetData τ).dihedralDeriv f k *
471 localEdgeLengthDirectionalDeriv K η τ k))
472 =
473 ∑ k : Fin 6,
474 localEdgeLengthDirectionalDeriv K η τ k *
475 (∑ f : Fin 6,
476 Real.sqrt ((K.tet τ).sqEdge f) *
477 ((triangulationSchlaefliData_of_incidence K hK).tetData τ).dihedralDeriv f k) := by
478 simp_rw [Finset.mul_sum]
479 rw [Finset.sum_comm]
480 refine Finset.sum_congr rfl ?_
481 intro k _
482 refine Finset.sum_congr rfl ?_
483 intro f _
484 ring
485 _ = ∑ k : Fin 6, localEdgeLengthDirectionalDeriv K η τ k * 0 := by
486 refine Finset.sum_congr rfl ?_
487 intro k _
488 rw [((triangulationSchlaefliData_of_incidence K hK).tetData τ).schlaefli k]
489 _ = 0 := by simp
490
491/-- A local angle package whose values are the edge-length chain-rule values.
492The remaining local analytic obligation is the `HasDerivAt` proof tying the
493actual cofactor/arccos angle to this closed-form chain-rule value. -/
494structure LocalAngleLengthChainRulePackage
495 (K : Triangulation3D) (hK : IncidenceConsistent K) where
496 angle_hasDerivAt :
497 ∀ (η : VertexPotential K) (τ : Fin K.nT) (f : Fin 6),
498 HasDerivAt
499 (fun t : ℝ => tetDihedralAngleUnderConformal K (linePotential K η t) τ f)
500 (localAngleLengthChainDeriv K hK η τ f) 0
501
502/-- The squared-edge chain-rule form that follows directly from the explicit
503cofactor/arccos coordinate derivative formulas. -/
504structure LocalAngleSqEdgeChainRulePackage
505 (K : Triangulation3D) where
506 angle_hasDerivAt :
507 ∀ (η : VertexPotential K) (τ : Fin K.nT) (f : Fin 6),
508 HasDerivAt
509 (fun t : ℝ => tetDihedralAngleUnderConformal K (linePotential K η t) τ f)
510 (localAngleSqEdgeChainDeriv K η τ f) 0
511
512def localAngleSqEdgeChainRulePackage_of_flat
513 (K : Triangulation3D) (hK : IncidenceConsistent K)
514 (h_flat : FlatConfiguration K hK) :
515 LocalAngleSqEdgeChainRulePackage K where
516 angle_hasDerivAt := by
517 intro η τ f
518 let T := K.tet τ
519 let F : CayleyMengerPolynomial.SqEdges → ℝ :=
520 fun a => DihedralDerivatives.dihedralAngle3Sq a f
521 let v : CayleyMengerPolynomial.SqEdges :=
522 fun k => conformalLocalSqEdgeDirectionalDeriv K η τ k
523 have hEndpoint : dihedralCos3Sq T.sqEdge f ≠ -1 ∧ dihedralCos3Sq T.sqEdge f ≠ 1 := by
524 simpa [T] using h_flat.local_arccos_endpoint_free τ f
525 have hAngle : ContDiffAt ℝ 1 F T.sqEdge := by
526 simpa [F, T] using dihedralAngle3Sq_contDiffAt_nonDegenerate (K.tet τ) f 1
527 (h_flat.local_arccos_endpoint_free τ f)
528 have hDiff : DifferentiableAt ℝ F T.sqEdge :=
529 hAngle.differentiableAt (by simp)
530 have hF : HasFDerivAt F (fderiv ℝ F T.sqEdge) T.sqEdge :=
531 hDiff.hasFDerivAt
532 have hbase : conformalTetSqEdges K (linePotential K η 0) τ = T.sqEdge := by
533 simpa [linePotential_zero K η, T] using
534 ReggeActionSmoothness.conformalTetSqEdges_zero K τ
535 have hF' : HasFDerivAt F (fderiv ℝ F T.sqEdge)
536 (conformalTetSqEdges K (linePotential K η 0) τ) := by
537 simpa [hbase] using hF
538 have hgamma : HasDerivAt
539 (fun t : ℝ => conformalTetSqEdges K (linePotential K η t) τ) v 0 := by
540 simpa [v] using conformalTetSqEdges_hasDerivAt_line_zero K η τ
541 have hcomp := HasFDerivAt.comp_hasDerivAt
542 (x := (0 : ℝ))
543 (f := fun t : ℝ => conformalTetSqEdges K (linePotential K η t) τ)
544 (l := F)
545 hF' hgamma
546 have hvalue :
547 (fderiv ℝ F T.sqEdge) v = localAngleSqEdgeChainDeriv K η τ f := by
548 unfold localAngleSqEdgeChainDeriv
549 calc
550 (fderiv ℝ F T.sqEdge) v
551 = ∑ k : Fin 6,
552 v k * (fderiv ℝ F T.sqEdge)
553 (Pi.single (M := fun _ : Fin 6 => ℝ) k (1 : ℝ)) := by
554 exact continuousLinearMap_apply_eq_sum_single (fderiv ℝ F T.sqEdge) v
555 _ = ∑ k : Fin 6,
556 dihedralClosedDerivSq (K.tet τ) f k *
557 conformalLocalSqEdgeDirectionalDeriv K η τ k := by
558 refine Finset.sum_congr rfl ?_
559 intro k _
560 have hcoord :=
561 fderiv_dihedralAngle3Sq_apply_single (K.tet τ) f k
562 (h_flat.local_arccos_endpoint_free τ f)
563 simp [F, T, v, hcoord, mul_comm]
564 rw [hvalue] at hcomp
565 simpa [F, Function.comp_def, tetDihedralAngleUnderConformal] using hcomp
566
567def localAngleLengthChainRulePackage_of_sqEdge
568 (K : Triangulation3D) (hK : IncidenceConsistent K)
569 (S : LocalAngleSqEdgeChainRulePackage K) :
570 LocalAngleLengthChainRulePackage K hK where
571 angle_hasDerivAt := by
572 intro η τ f
573 have h := S.angle_hasDerivAt η τ f
574 rw [localAngleLengthChainDeriv_eq_sqEdgeChainDeriv K hK η τ f]
575 exact h
576
577def localDihedralDirectionalDerivativePackage_of_lengthChain
578 (K : Triangulation3D) (hK : IncidenceConsistent K)
579 (L : LocalAngleLengthChainRulePackage K hK) :
580 LocalDihedralDirectionalDerivativePackage K where
581 angleDeriv := localAngleLengthChainDeriv K hK
582 angle_hasDerivAt := L.angle_hasDerivAt
583
584def deficitDirectionalDerivFromLocalAngles
585 (K : Triangulation3D) (A : LocalDihedralDirectionalDerivativePackage K)
586 (η : VertexPotential K) (e : Fin K.nE) : ℝ :=
587 - ∑ τ : Fin K.nT,
588 match K.edgeInTet e τ with
589 | none => 0
590 | some f => A.angleDeriv η τ f
591
592/-- Directional derivative package for deficit angles. The cancellation field
593is exactly the global Schläfli contribution in the conformal direction. -/
594structure DeficitAngleDirectionalDerivativePackage
595 (K : Triangulation3D) (hK : IncidenceConsistent K) where
596 deficitDeriv : VertexPotential K → Fin K.nE → ℝ
597 deficit_hasDerivAt :
598 ∀ (η : VertexPotential K) (e : Fin K.nE),
599 HasDerivAt (fun t : ℝ => deficitAngle K (linePotential K η t) e)
600 (deficitDeriv η e) 0
601 schlaefli_cancellation :
602 ∀ η : VertexPotential K,
603 (∑ e : Fin K.nE,
604 hingeMeasureUnderConformal K hK (zeroPotential K) e * deficitDeriv η e) = 0
605
606theorem localDeficitAngleContribution_hasDerivAt_from_localAngles
607 (K : Triangulation3D) (A : LocalDihedralDirectionalDerivativePackage K)
608 (η : VertexPotential K) (e : Fin K.nE) (τ : Fin K.nT) :
609 HasDerivAt
610 (fun t : ℝ => localDeficitAngleContribution K (linePotential K η t) e τ)
611 (match K.edgeInTet e τ with
612 | none => 0
613 | some f => A.angleDeriv η τ f) 0 := by
614 unfold localDeficitAngleContribution
615 cases h : K.edgeInTet e τ with
616 | none =>
617 simpa [h] using (hasDerivAt_const (0 : ℝ) (0 : ℝ))
618 | some f =>
619 simpa [h] using A.angle_hasDerivAt η τ f
620
621theorem deficitAngle_hasDerivAt_from_localAngles
622 (K : Triangulation3D) (A : LocalDihedralDirectionalDerivativePackage K)
623 (η : VertexPotential K) (e : Fin K.nE) :
624 HasDerivAt
625 (fun t : ℝ => deficitAngle K (linePotential K η t) e)
626 (deficitDirectionalDerivFromLocalAngles K A η e) 0 := by
627 unfold deficitAngle deficitDirectionalDerivFromLocalAngles
628 have hsum : HasDerivAt
629 (∑ τ : Fin K.nT,
630 fun t : ℝ => localDeficitAngleContribution K (linePotential K η t) e τ)
631 (∑ τ : Fin K.nT,
632 match K.edgeInTet e τ with
633 | none => 0
634 | some f => A.angleDeriv η τ f) 0 := by
635 have hsum' :=
636 HasDerivAt.sum
637 (u := Finset.univ)
638 (A := fun τ t => localDeficitAngleContribution K (linePotential K η t) e τ)
639 (A' := fun τ =>
640 match K.edgeInTet e τ with
641 | none => 0
642 | some f => A.angleDeriv η τ f)
643 (x := 0)
644 (fun τ _ => localDeficitAngleContribution_hasDerivAt_from_localAngles K A η e τ)
645 simpa using hsum'
646 have hconst : HasDerivAt (fun _t : ℝ => 2 * Real.pi) 0 0 :=
647 hasDerivAt_const 0 (2 * Real.pi)
648 have hsub := hconst.sub hsum
649 convert hsub using 1
650 · ext t
651 simp [Pi.sub_apply, Finset.sum_apply]
652 · ring
653
654def deficitPackage_of_localAngles
655 (K : Triangulation3D) (hK : IncidenceConsistent K)
656 (A : LocalDihedralDirectionalDerivativePackage K)
657 (hCancel :
658 ∀ η : VertexPotential K,
659 (∑ e : Fin K.nE,
660 hingeMeasureUnderConformal K hK (zeroPotential K) e *
661 deficitDirectionalDerivFromLocalAngles K A η e) = 0) :
662 DeficitAngleDirectionalDerivativePackage K hK where
663 deficitDeriv := deficitDirectionalDerivFromLocalAngles K A
664 deficit_hasDerivAt := deficitAngle_hasDerivAt_from_localAngles K A
665 schlaefli_cancellation := hCancel
666
667/-- The exact Schläfli cancellation needed by the conformal first variation
668after the local dihedral directional derivatives have been constructed. -/
669def ConformalSchlaefliCancellation
670 (K : Triangulation3D) (hK : IncidenceConsistent K)
671 (A : LocalDihedralDirectionalDerivativePackage K) : Prop :=
672 ∀ η : VertexPotential K,
673 (∑ e : Fin K.nE,
674 hingeMeasureUnderConformal K hK (zeroPotential K) e *
675 deficitDirectionalDerivFromLocalAngles K A η e) = 0
676
677/-- Global incidence bookkeeping needed to turn the edge-indexed deficit
678variation into the sum of local tetrahedral Schläfli sums. -/
679def ConformalSchlaefliIncidenceBookkeeping
680 (K : Triangulation3D) (hK : IncidenceConsistent K)
681 (A : LocalDihedralDirectionalDerivativePackage K) : Prop :=
682 ∀ η : VertexPotential K,
683 (∑ e : Fin K.nE,
684 hingeMeasureUnderConformal K hK (zeroPotential K) e *
685 deficitDirectionalDerivFromLocalAngles K A η e) =
686 - ∑ τ : Fin K.nT,
687 ∑ f : Fin 6,
688 Real.sqrt ((K.tet τ).sqEdge f) * A.angleDeriv η τ f
689
690/-- Incidence partition certificate: summing a local edge-slot weight over
691global edges and tetrahedra is the same as summing it directly over local
692tetrahedral edge slots, with matching flat edge lengths.
693
694`IncidenceConsistent.localEdge_complete` gives existence of a global edge for
695each local slot. Exact reindexing also needs uniqueness/no-duplication, so it
696is recorded here as the actual bookkeeping theorem needed downstream. -/
697structure IncidenceEdgeSlotBookkeeping
698 (K : Triangulation3D) (hK : IncidenceConsistent K) where
699 sum_match :
700 ∀ w : Fin K.nT → Fin 6 → ℝ,
701 (∑ e : Fin K.nE,
702 globalEdgeLength K hK e *
703 (∑ τ : Fin K.nT,
704 match K.edgeInTet e τ with
705 | none => 0
706 | some f => w τ f)) =
707 ∑ τ : Fin K.nT,
708 ∑ f : Fin 6,
709 Real.sqrt ((K.tet τ).sqEdge f) * w τ f
710
711/-- The intended concrete incidence class for edge-slot bookkeeping: every
712local tetrahedral edge slot `(τ,f)` is represented by exactly one global edge,
713and the incidence map hits that slot iff the global edge is that representative. -/
714structure IncidenceEdgeSlotPartition
715 (K : Triangulation3D) (hK : IncidenceConsistent K) where
716 localEdgeOf : Fin K.nT → Fin 6 → Fin K.nE
717 edgeInTet_iff :
718 ∀ e τ f, K.edgeInTet e τ = some f ↔ e = localEdgeOf τ f
719
720theorem IncidenceEdgeSlotPartition.localEdgeOf_incident
721 {K : Triangulation3D} {hK : IncidenceConsistent K}
722 (P : IncidenceEdgeSlotPartition K hK) (τ : Fin K.nT) (f : Fin 6) :
723 K.edgeInTet (P.localEdgeOf τ f) τ = some f :=
724 (P.edgeInTet_iff (P.localEdgeOf τ f) τ f).2 rfl
725
726theorem IncidenceEdgeSlotPartition.global_length_localEdgeOf
727 {K : Triangulation3D} {hK : IncidenceConsistent K}
728 (P : IncidenceEdgeSlotPartition K hK) (τ : Fin K.nT) (f : Fin 6) :
729 globalEdgeLength K hK (P.localEdgeOf τ f) =
730 Real.sqrt ((K.tet τ).sqEdge f) := by
731 unfold globalEdgeLength
732 rw [← hK.local_sqEdge_eq_global (P.localEdgeOf τ f) τ f
733 (P.localEdgeOf_incident τ f)]
734
735theorem IncidenceEdgeSlotPartition.edge_sum_for_tet
736 {K : Triangulation3D} {hK : IncidenceConsistent K}
737 (P : IncidenceEdgeSlotPartition K hK)
738 (w : Fin K.nT → Fin 6 → ℝ) (τ : Fin K.nT) :
739 (∑ e : Fin K.nE,
740 globalEdgeLength K hK e *
741 (match K.edgeInTet e τ with
742 | none => 0
743 | some f => w τ f)) =
744 ∑ f : Fin 6, Real.sqrt ((K.tet τ).sqEdge f) * w τ f := by
745 calc
746 (∑ e : Fin K.nE,
747 globalEdgeLength K hK e *
748 (match K.edgeInTet e τ with
749 | none => 0
750 | some f => w τ f))
751 =
752 ∑ e : Fin K.nE,
753 ∑ f : Fin 6,
754 if K.edgeInTet e τ = some f then
755 globalEdgeLength K hK e * w τ f
756 else 0 := by
757 refine Finset.sum_congr rfl ?_
758 intro e _
759 cases h : K.edgeInTet e τ with
760 | none =>
761 simp
762 | some f0 =>
763 simp
764 _ = ∑ f : Fin 6,
765 ∑ e : Fin K.nE,
766 if K.edgeInTet e τ = some f then
767 globalEdgeLength K hK e * w τ f
768 else 0 := by
769 rw [Finset.sum_comm]
770 _ = ∑ f : Fin 6,
771 globalEdgeLength K hK (P.localEdgeOf τ f) * w τ f := by
772 refine Finset.sum_congr rfl ?_
773 intro f _
774 have hsum := Finset.sum_eq_single
775 (s := Finset.univ)
776 (f := fun e : Fin K.nE =>
777 (if K.edgeInTet e τ = some f then
778 globalEdgeLength K hK e * w τ f
779 else 0 : ℝ))
780 (P.localEdgeOf τ f) ?_ ?_
781 · simpa [P.localEdgeOf_incident τ f] using hsum
782 · intro e _ he_ne
783 have hnot : K.edgeInTet e τ ≠ some f := by
784 intro h
785 exact he_ne ((P.edgeInTet_iff e τ f).1 h)
786 simp [hnot]
787 · intro hnot_mem
788 exact (hnot_mem (Finset.mem_univ _)).elim
789 _ = ∑ f : Fin 6, Real.sqrt ((K.tet τ).sqEdge f) * w τ f := by
790 refine Finset.sum_congr rfl ?_
791 intro f _
792 rw [P.global_length_localEdgeOf τ f]
793
794def incidenceEdgeSlotBookkeeping_of_partition
795 (K : Triangulation3D) (hK : IncidenceConsistent K)
796 (P : IncidenceEdgeSlotPartition K hK) :
797 IncidenceEdgeSlotBookkeeping K hK where
798 sum_match := by
799 intro w
800 calc
801 (∑ e : Fin K.nE,
802 globalEdgeLength K hK e *
803 (∑ τ : Fin K.nT,
804 match K.edgeInTet e τ with
805 | none => 0
806 | some f => w τ f))
807 =
808 ∑ e : Fin K.nE,
809 ∑ τ : Fin K.nT,
810 globalEdgeLength K hK e *
811 (match K.edgeInTet e τ with
812 | none => 0
813 | some f => w τ f) := by
814 refine Finset.sum_congr rfl ?_
815 intro e _
816 rw [Finset.mul_sum]
817 _ = ∑ τ : Fin K.nT,
818 ∑ e : Fin K.nE,
819 globalEdgeLength K hK e *
820 (match K.edgeInTet e τ with
821 | none => 0
822 | some f => w τ f) := by
823 rw [Finset.sum_comm]
824 _ = ∑ τ : Fin K.nT,
825 ∑ f : Fin 6,
826 Real.sqrt ((K.tet τ).sqEdge f) * w τ f := by
827 refine Finset.sum_congr rfl ?_
828 intro τ _
829 exact P.edge_sum_for_tet w τ
830
831theorem conformalSchlaefliIncidenceBookkeeping_of_edgeSlotBookkeeping
832 (K : Triangulation3D) (hK : IncidenceConsistent K)
833 (A : LocalDihedralDirectionalDerivativePackage K)
834 (hBook : IncidenceEdgeSlotBookkeeping K hK) :
835 ConformalSchlaefliIncidenceBookkeeping K hK A := by
836 intro η
837 unfold deficitDirectionalDerivFromLocalAngles
838 calc
839 (∑ e : Fin K.nE,
840 hingeMeasureUnderConformal K hK (zeroPotential K) e *
841 (-∑ τ : Fin K.nT,
842 match K.edgeInTet e τ with
843 | none => 0
844 | some f => A.angleDeriv η τ f))
845 =
846 - (∑ e : Fin K.nE,
847 globalEdgeLength K hK e *
848 (∑ τ : Fin K.nT,
849 match K.edgeInTet e τ with
850 | none => 0
851 | some f => A.angleDeriv η τ f)) := by
852 unfold hingeMeasureUnderConformal globalEdgeLength zeroPotential
853 rw [← Finset.sum_neg_distrib]
854 refine Finset.sum_congr rfl ?_
855 intro e _
856 simp
857 _ = - (∑ τ : Fin K.nT,
858 ∑ f : Fin 6,
859 Real.sqrt ((K.tet τ).sqEdge f) * A.angleDeriv η τ f) := by
860 rw [hBook.sum_match (fun τ f => A.angleDeriv η τ f)]
861
862theorem conformalSchlaefliCancellation_of_lengthChain_of_bookkeeping
863 (K : Triangulation3D) (hK : IncidenceConsistent K)
864 (L : LocalAngleLengthChainRulePackage K hK)
865 (hBook :
866 ConformalSchlaefliIncidenceBookkeeping K hK
867 (localDihedralDirectionalDerivativePackage_of_lengthChain K hK L)) :
868 ConformalSchlaefliCancellation K hK
869 (localDihedralDirectionalDerivativePackage_of_lengthChain K hK L) := by
870 intro η
871 rw [hBook η]
872 have hlocal : ∀ τ : Fin K.nT,
873 (∑ f : Fin 6,
874 Real.sqrt ((K.tet τ).sqEdge f) *
875 (localDihedralDirectionalDerivativePackage_of_lengthChain K hK L).angleDeriv η τ f) = 0 := by
876 intro τ
877 exact local_conformal_schlaefli_cancellation K hK η τ
878 simp_rw [hlocal]
879 simp
880
881def deficitPackage_of_conformalSchlaefliCancellation
882 (K : Triangulation3D) (hK : IncidenceConsistent K)
883 (A : LocalDihedralDirectionalDerivativePackage K)
884 (hCancel : ConformalSchlaefliCancellation K hK A) :
885 DeficitAngleDirectionalDerivativePackage K hK :=
886 deficitPackage_of_localAngles K hK A hCancel
887
888theorem directionalFirstVariationFormula_of_deficitPackage
889 (K : Triangulation3D) (hK : IncidenceConsistent K)
890 (D : DeficitAngleDirectionalDerivativePackage K hK) :
891 ReggeActionDirectionalFirstVariationFormula K hK where
892 directional_formula := by
893 intro η
894 unfold reggeAction
895 have hedge :
896 ∀ e : Fin K.nE,
897 HasDerivAt
898 (fun t : ℝ =>
899 hingeMeasureUnderConformal K hK (linePotential K η t) e *
900 deficitAngle K (linePotential K η t) e)
901 (hingeMeasureDirectionalDeriv K hK η e *
902 deficitAngle K (zeroPotential K) e +
903 hingeMeasureUnderConformal K hK (zeroPotential K) e *
904 D.deficitDeriv η e) 0 := by
905 intro e
906 have hL := hingeMeasureUnderConformal_hasDerivAt_line_zero K hK η e
907 have hδ := D.deficit_hasDerivAt η e
908 have hprod := hL.mul hδ
909 simpa [linePotential_zero K η, mul_comm, mul_left_comm, mul_assoc] using hprod
910 have hsum : HasDerivAt
911 (∑ e : Fin K.nE,
912 fun t : ℝ =>
913 hingeMeasureUnderConformal K hK (linePotential K η t) e *
914 deficitAngle K (linePotential K η t) e)
915 (∑ e : Fin K.nE,
916 (hingeMeasureDirectionalDeriv K hK η e *
917 deficitAngle K (zeroPotential K) e +
918 hingeMeasureUnderConformal K hK (zeroPotential K) e *
919 D.deficitDeriv η e)) 0 := by
920 have hsum' :=
921 HasDerivAt.sum
922 (u := Finset.univ)
923 (A := fun e t =>
924 hingeMeasureUnderConformal K hK (linePotential K η t) e *
925 deficitAngle K (linePotential K η t) e)
926 (A' := fun e =>
927 hingeMeasureDirectionalDeriv K hK η e *
928 deficitAngle K (zeroPotential K) e +
929 hingeMeasureUnderConformal K hK (zeroPotential K) e *
930 D.deficitDeriv η e)
931 (x := 0)
932 (fun e _ => hedge e)
933 simpa [Finset.sum_apply] using hsum'
934 have htarget :
935 (∑ e : Fin K.nE,
936 (hingeMeasureDirectionalDeriv K hK η e *
937 deficitAngle K (zeroPotential K) e +
938 hingeMeasureUnderConformal K hK (zeroPotential K) e *
939 D.deficitDeriv η e)) =
940 ∑ e : Fin K.nE,
941 hingeMeasureDirectionalDeriv K hK η e *
942 deficitAngle K (zeroPotential K) e := by
943 rw [Finset.sum_add_distrib, D.schlaefli_cancellation η]
944 ring
945 rw [htarget] at hsum
946 convert hsum using 1
947 ext t
948 simp
949
950theorem firstVariationFormula_of_directionalFormula
951 (K : Triangulation3D) (hK : IncidenceConsistent K)
952 (h_flat : FlatConfiguration K hK)
953 (hdir : ReggeActionDirectionalFirstVariationFormula K hK) :
954 ReggeActionFirstVariationFormula K hK where
955 firstVariation_formula := by
956 intro η
957 have hleft := reggeAction_along_line_hasDerivAt_fderiv K hK h_flat η
958 have hright := hdir.directional_formula η
959 exact hleft.unique hright
960
961theorem directionalCritical_of_firstVariationFormula_of_zeroDeficit
962 (K : Triangulation3D) (hK : IncidenceConsistent K)
963 (hZero : GlobalZeroDeficitAtFlat K)
964 (hFormula : ReggeActionFirstVariationFormula K hK) :
965 ReggeActionDirectionalCriticalAtZero K hK := by
966 intro η
967 rw [hFormula.firstVariation_formula η]
968 apply Finset.sum_eq_zero
969 intro e _
970 rw [hZero e]
971 ring
972
973theorem reggeActionCriticalAtZero_of_firstVariationFormula_of_zeroDeficit
974 (K : Triangulation3D) (hK : IncidenceConsistent K)
975 (hZero : GlobalZeroDeficitAtFlat K)
976 (hFormula : ReggeActionFirstVariationFormula K hK) :
977 ReggeActionCriticalAtZero K hK :=
978 reggeActionCriticalAtZero_of_directional K hK
979 (directionalCritical_of_firstVariationFormula_of_zeroDeficit K hK hZero hFormula)
980
981/-- Named first-variation input. The intended lower-level proof is:
982differentiate the hinge-length factor and local dihedral factors, use zero
983deficit for the hinge term, then use the global Schläfli identity for the
984dihedral term. -/
985structure ReggeActionFirstVariationInput
986 (K : Triangulation3D) (hK : IncidenceConsistent K)
987 (_h_flat : FlatConfiguration K hK) where
988 firstVariation_zero : ReggeActionCriticalAtZero K hK
989
990def reggeActionFirstVariationInput_of_directional
991 (K : Triangulation3D) (hK : IncidenceConsistent K)
992 (h_flat : FlatConfiguration K hK)
993 (hdir : ReggeActionDirectionalCriticalAtZero K hK) :
994 ReggeActionFirstVariationInput K hK h_flat where
995 firstVariation_zero := reggeActionCriticalAtZero_of_directional K hK hdir
996
997def reggeActionFirstVariationInput_of_firstVariationFormula
998 (K : Triangulation3D) (hK : IncidenceConsistent K)
999 (h_flat : FlatConfiguration K hK)
1000 (hFormula : ReggeActionFirstVariationFormula K hK) :
1001 ReggeActionFirstVariationInput K hK h_flat where
1002 firstVariation_zero :=
1003 reggeActionCriticalAtZero_of_firstVariationFormula_of_zeroDeficit
1004 K hK h_flat.flat_deficit_zero hFormula
1005
1006def reggeActionFirstVariationInput_of_localAngles
1007 (K : Triangulation3D) (hK : IncidenceConsistent K)
1008 (h_flat : FlatConfiguration K hK)
1009 (A : LocalDihedralDirectionalDerivativePackage K)
1010 (hCancel : ConformalSchlaefliCancellation K hK A) :
1011 ReggeActionFirstVariationInput K hK h_flat :=
1012 reggeActionFirstVariationInput_of_firstVariationFormula K hK h_flat
1013 (firstVariationFormula_of_directionalFormula K hK h_flat
1014 (directionalFirstVariationFormula_of_deficitPackage K hK
1015 (deficitPackage_of_conformalSchlaefliCancellation K hK A hCancel)))
1016
1017def reggeActionFirstVariationInput_of_conformalSchlaefliCancellation
1018 (K : Triangulation3D) (hK : IncidenceConsistent K)
1019 (h_flat : FlatConfiguration K hK)
1020 (hCancel : ConformalSchlaefliCancellation K hK
1021 (localDihedralDirectionalDerivativePackage_of_flat K hK h_flat)) :
1022 ReggeActionFirstVariationInput K hK h_flat :=
1023 reggeActionFirstVariationInput_of_localAngles K hK h_flat
1024 (localDihedralDirectionalDerivativePackage_of_flat K hK h_flat) hCancel
1025
1026def reggeActionFirstVariationInput_of_incidenceBookkeeping
1027 (K : Triangulation3D) (hK : IncidenceConsistent K)
1028 (h_flat : FlatConfiguration K hK)
1029 (hBook : ConformalSchlaefliIncidenceBookkeeping K hK
1030 (localDihedralDirectionalDerivativePackage_of_lengthChain K hK
1031 (localAngleLengthChainRulePackage_of_sqEdge K hK
1032 (localAngleSqEdgeChainRulePackage_of_flat K hK h_flat)))) :
1033 ReggeActionFirstVariationInput K hK h_flat :=
1034 reggeActionFirstVariationInput_of_localAngles K hK h_flat
1035 (localDihedralDirectionalDerivativePackage_of_lengthChain K hK
1036 (localAngleLengthChainRulePackage_of_sqEdge K hK
1037 (localAngleSqEdgeChainRulePackage_of_flat K hK h_flat)))
1038 (conformalSchlaefliCancellation_of_lengthChain_of_bookkeeping K hK
1039 (localAngleLengthChainRulePackage_of_sqEdge K hK
1040 (localAngleSqEdgeChainRulePackage_of_flat K hK h_flat))
1041 hBook)
1042
1043def reggeActionFirstVariationInput_of_edgeSlotBookkeeping
1044 (K : Triangulation3D) (hK : IncidenceConsistent K)
1045 (h_flat : FlatConfiguration K hK)
1046 (hBook : IncidenceEdgeSlotBookkeeping K hK) :
1047 ReggeActionFirstVariationInput K hK h_flat :=
1048 reggeActionFirstVariationInput_of_incidenceBookkeeping K hK h_flat
1049 (conformalSchlaefliIncidenceBookkeeping_of_edgeSlotBookkeeping K hK
1050 (localDihedralDirectionalDerivativePackage_of_lengthChain K hK
1051 (localAngleLengthChainRulePackage_of_sqEdge K hK
1052 (localAngleSqEdgeChainRulePackage_of_flat K hK h_flat)))
1053 hBook)
1054
1055def reggeActionFirstVariationInput_of_edgeSlotPartition
1056 (K : Triangulation3D) (hK : IncidenceConsistent K)
1057 (h_flat : FlatConfiguration K hK)
1058 (P : IncidenceEdgeSlotPartition K hK) :
1059 ReggeActionFirstVariationInput K hK h_flat :=
1060 reggeActionFirstVariationInput_of_edgeSlotBookkeeping K hK h_flat
1061 (incidenceEdgeSlotBookkeeping_of_partition K hK P)
1062
1063/-- Phase-C first-variation theorem, conditional on the named analytic
1064first-variation input. -/
1065theorem reggeAction_firstVariation_zero
1066 (K : Triangulation3D) (hK : IncidenceConsistent K)
1067 (h_flat : FlatConfiguration K hK)
1068 (h_first : ReggeActionFirstVariationInput K hK h_flat) :
1069 fderiv ℝ (reggeAction K hK) (zeroPotential K) = 0 :=
1070 h_first.firstVariation_zero
1071
1072/-- First variation of the nonlinear remainder. This is recorded as a
1073separate named input because proving it directly requires the derivative of
1074the finite-dimensional quadratic form at zero in the same analytic universe
1075as the full action. -/
1076structure ReggeActionRemainderFirstVariationInput
1077 (K : Triangulation3D) (hK : IncidenceConsistent K)
1078 (H : Fin K.nV → Fin K.nV → ℝ) where
1079 remainder_firstVariation_zero :
1080 fderiv ℝ (reggeActionRemainder K hK H) (zeroPotential K) = 0
1081
1082theorem reggeActionRemainder_fderiv_zero
1083 (K : Triangulation3D) (hK : IncidenceConsistent K)
1084 (H : Fin K.nV → Fin K.nV → ℝ)
1085 (h_rem : ReggeActionRemainderFirstVariationInput K hK H) :
1086 fderiv ℝ (reggeActionRemainder K hK H) (zeroPotential K) = 0 :=
1087 h_rem.remainder_firstVariation_zero
1088
1089private theorem hasFDerivAt_finset_sum_zero
1090 {ι E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
1091 (s : Finset ι) (f : ι → E → ℝ) (x : E)
1092 (hf : ∀ i ∈ s, HasFDerivAt (f i) (0 : E →L[ℝ] ℝ) x) :
1093 HasFDerivAt (fun y => s.sum (fun i => f i y)) (0 : E →L[ℝ] ℝ) x := by
1094 classical
1095 revert hf
1096 refine Finset.induction_on s ?_ ?_
1097 · intro _hf
1098 change HasFDerivAt (fun _y : E => (0 : ℝ)) (0 : E →L[ℝ] ℝ) x
1099 simpa using
1100 (hasFDerivAt_const (x := x) (c := (0 : ℝ)))
1101 · intro a s ha ih hf
1102 have hfa : HasFDerivAt (f a) (0 : E →L[ℝ] ℝ) x :=
1103 hf a (by simp [ha])
1104 have hfs : HasFDerivAt (fun y => s.sum (fun i => f i y)) (0 : E →L[ℝ] ℝ) x :=
1105 ih (by
1106 intro i hi
1107 exact hf i (by simp [hi]))
1108 simpa [ha] using hfa.add hfs
1109
1110private theorem hessianQuadratic_term_hasFDerivAt_zero
1111 (K : Triangulation3D) (H : Fin K.nV → Fin K.nV → ℝ)
1112 (i j : Fin K.nV) :
1113 HasFDerivAt
1114 (fun ξ : VertexPotential K => H i j * ξ i * ξ j)
1115 (0 : VertexPotential K →L[ℝ] ℝ)
1116 (zeroPotential K) := by
1117 let evalI : VertexPotential K →L[ℝ] ℝ :=
1118 ContinuousLinearMap.proj (R := ℝ) (φ := fun _ : Fin K.nV => ℝ) i
1119 let evalJ : VertexPotential K →L[ℝ] ℝ :=
1120 ContinuousLinearMap.proj (R := ℝ) (φ := fun _ : Fin K.nV => ℝ) j
1121 have hi : HasFDerivAt (fun ξ : VertexPotential K => ξ i) evalI (zeroPotential K) := by
1122 simpa [evalI] using evalI.hasFDerivAt
1123 have hj : HasFDerivAt (fun ξ : VertexPotential K => ξ j) evalJ (zeroPotential K) := by
1124 simpa [evalJ] using evalJ.hasFDerivAt
1125 have hHi : HasFDerivAt (fun ξ : VertexPotential K => H i j * ξ i)
1126 (H i j • evalI) (zeroPotential K) := by
1127 simpa [mul_comm, mul_left_comm, mul_assoc] using hi.const_mul (H i j)
1128 have h := hHi.mul hj
1129 convert h using 1
1130 · ext η
1131 simp [zeroPotential]
1132
1133/-- The quadratic Hessian form has zero first derivative at the zero potential. -/
1134theorem hessianQuadratic_hasFDerivAt_zero
1135 (K : Triangulation3D) (H : Fin K.nV → Fin K.nV → ℝ) :
1136 HasFDerivAt
1137 (fun ξ : VertexPotential K => hessianQuadratic H ξ)
1138 (0 : VertexPotential K →L[ℝ] ℝ)
1139 (zeroPotential K) := by
1140 unfold hessianQuadratic zeroPotential
1141 apply hasFDerivAt_finset_sum_zero
1142 intro i _hi
1143 apply hasFDerivAt_finset_sum_zero
1144 intro j _hj
1145 simpa [zeroPotential] using hessianQuadratic_term_hasFDerivAt_zero K H i j
1146
1147/-- The scaled quadratic Hessian term used in the Regge Taylor split also has
1148zero first derivative at the zero potential. -/
1149theorem half_hessianQuadratic_hasFDerivAt_zero
1150 (K : Triangulation3D) (H : Fin K.nV → Fin K.nV → ℝ) :
1151 HasFDerivAt
1152 (fun ξ : VertexPotential K => (1 / 2 : ℝ) * hessianQuadratic H ξ)
1153 (0 : VertexPotential K →L[ℝ] ℝ)
1154 (zeroPotential K) := by
1155 simpa using (hessianQuadratic_hasFDerivAt_zero K H).const_mul (1 / 2 : ℝ)
1156
1157/-- The nonlinear remainder first-variation input follows from the full Regge
1158first-variation input. The subtracted constant has zero derivative and the
1159subtracted quadratic Hessian term has zero derivative at the flat point. -/
1160def reggeActionRemainderFirstVariationInput_of_firstVariation
1161 (K : Triangulation3D) (hK : IncidenceConsistent K)
1162 (h_flat : FlatConfiguration K hK)
1163 (H : Fin K.nV → Fin K.nV → ℝ)
1164 (h_first : ReggeActionFirstVariationInput K hK h_flat) :
1165 ReggeActionRemainderFirstVariationInput K hK H where
1166 remainder_firstVariation_zero := by
1167 have hActionDiff : DifferentiableAt ℝ (reggeAction K hK) (zeroPotential K) :=
1168 h_flat.action_contDiff_at_zero.differentiableAt (by simp)
1169 have hAction :
1170 HasFDerivAt (reggeAction K hK)
1171 (0 : VertexPotential K →L[ℝ] ℝ) (zeroPotential K) := by
1172 have h := hActionDiff.hasFDerivAt
1173 rw [h_first.firstVariation_zero] at h
1174 exact h
1175 have hConst : HasFDerivAt
1176 (fun _ξ : VertexPotential K => reggeAction K hK (zeroPotential K))
1177 (0 : VertexPotential K →L[ℝ] ℝ)
1178 (zeroPotential K) := by
1179 simpa using
1180 (hasFDerivAt_const
1181 (x := zeroPotential K)
1182 (c := reggeAction K hK (zeroPotential K)))
1183 have hQuad := half_hessianQuadratic_hasFDerivAt_zero K H
1184 have hRemRaw :=
1185 (hAction.sub hConst).sub hQuad
1186 have hRem :
1187 HasFDerivAt
1188 (fun ξ : VertexPotential K =>
1189 reggeAction K hK ξ -
1190 reggeAction K hK (zeroPotential K) -
1191 (1 / 2 : ℝ) * hessianQuadratic H ξ)
1192 (0 : VertexPotential K →L[ℝ] ℝ)
1193 (zeroPotential K) := by
1194 convert hRemRaw using 1
1195 · simp
1196 convert hRem.fderiv using 1
1197
1198end
1199
1200end ReggeActionFirstVariation
1201end Geometry
1202end IndisputableMonolith
1203