IndisputableMonolith.Gravity.Analysis.SRSTTFirstVariation4D
IndisputableMonolith/Gravity/Analysis/SRSTTFirstVariation4D.lean · 482 lines · 36 declarations
show as:
view math explainer →
1import Mathlib
2import IndisputableMonolith.Gravity.Analysis.SRSConvergesEH4D
3
4/-!
5# TT directional first variation of the closed 4D midpoint Bloch symbol
6
7Derives the genuine cross-term / directional first variation of
8`exactMidpointBlochSymbol` in the Euclidean weak-field TT sector, then
9transports its torus-normalized continuum face via the banked
10`S_RS_converges_EH_4d_closed` Tendsto on `H+K` and `H-K` plus polarization.
11
12## Honesty (binding)
13
14* **THEOREM** only in the Euclidean weak-field TT sector of the closed
15 midpoint Bloch continuum face.
16* Explicitly **NOT** a source equation, **NOT** Ricci / null focusing,
17 and **NOT** GAP1 closure.
18* The exact missing future object is a concrete Recognition-derived
19 Freudenthal exact-J metric refinement / pullback identifying the sourced
20 response with this midpoint variation, followed by Lorentzian null-dyad
21 Ricci / stress transport.
22* Do not cite `PixelAreaModel`, `LocalNullPatch`,
23 `ObeysRSNullFieldEquation`, or the MODEL `exactJActionOnMesh` of
24 `RecognitionMeshExactJBridge4D` as an argument. (Transitively imported
25 modules may exist; they are not used here.)
26-/
27
28namespace IndisputableMonolith
29namespace Gravity
30namespace Analysis
31namespace SRSTTFirstVariation4D
32
33open Regge4DContinuumPreflight
34open ReggeExactFlatHessianBlochData4D
35open ReggeExactFlatHessianBlochSymbol4D
36open ReggeExactFlatHessianBlochTorusBridge4D
37open EdgeTTDecomposition4D
38open SRSConvergesEH4D
39open BigOperators Filter Topology
40
41set_option maxRecDepth 4096
42set_option maxHeartbeats 4000000
43
44noncomputable section
45
46abbrev Mat4 := Regge4DContinuumPreflight.Mat4
47abbrev Wave4 := Regge4DContinuumPreflight.Wave4
48abbrev CouplingIdx := ReggeExactFlatHessianBlochSymbol4D.CouplingIdx
49
50/-! ## §1. Frobenius pairing and edge-strain linearity -/
51
52/-- Euclidean Frobenius pairing on `4×4` matrices. -/
53def frobeniusPairing4D (H K : Mat4) : ℝ :=
54 ∑ i : Fin 4, ∑ j : Fin 4, H i j * K i j
55
56theorem frobeniusNormSq_eq_pairing_self (H : Mat4) :
57 frobeniusNormSq H = frobeniusPairing4D H H := rfl
58
59theorem edgeStrain_add (H K : Mat4) (D : Fin 4 → ℤ) :
60 edgeStrain (H + K) D = edgeStrain H D + edgeStrain K D := by
61 unfold edgeStrain
62 calc
63 ∑ i : Fin 4, ∑ j : Fin 4, (H + K) i j * (D i : ℝ) * (D j : ℝ)
64 = ∑ i : Fin 4, ∑ j : Fin 4,
65 (H i j * (D i : ℝ) * (D j : ℝ) +
66 K i j * (D i : ℝ) * (D j : ℝ)) := by
67 refine Finset.sum_congr rfl fun i _ =>
68 Finset.sum_congr rfl fun j _ => ?_
69 simp only [Matrix.add_apply]
70 ring
71 _ = ∑ i : Fin 4,
72 ((∑ j : Fin 4, H i j * (D i : ℝ) * (D j : ℝ)) +
73 ∑ j : Fin 4, K i j * (D i : ℝ) * (D j : ℝ)) := by
74 refine Finset.sum_congr rfl fun i _ => Finset.sum_add_distrib
75 _ = (∑ i : Fin 4, ∑ j : Fin 4, H i j * (D i : ℝ) * (D j : ℝ)) +
76 (∑ i : Fin 4, ∑ j : Fin 4, K i j * (D i : ℝ) * (D j : ℝ)) :=
77 Finset.sum_add_distrib
78
79theorem edgeStrain_smul (c : ℝ) (H : Mat4) (D : Fin 4 → ℤ) :
80 edgeStrain (c • H) D = c * edgeStrain H D := by
81 unfold edgeStrain
82 calc
83 ∑ i : Fin 4, ∑ j : Fin 4, (c • H) i j * (D i : ℝ) * (D j : ℝ)
84 = ∑ i : Fin 4, ∑ j : Fin 4,
85 c * (H i j * (D i : ℝ) * (D j : ℝ)) := by
86 refine Finset.sum_congr rfl fun i _ =>
87 Finset.sum_congr rfl fun j _ => ?_
88 simp only [Matrix.smul_apply, smul_eq_mul]
89 ring
90 _ = c * ∑ i : Fin 4, ∑ j : Fin 4, H i j * (D i : ℝ) * (D j : ℝ) := by
91 rw [Finset.mul_sum]
92 refine Finset.sum_congr rfl fun i _ => (Finset.mul_sum _ _ c).symm
93
94theorem edgeStrain_neg (H : Mat4) (D : Fin 4 → ℤ) :
95 edgeStrain (-H) D = -edgeStrain H D := by
96 simpa [neg_one_smul] using edgeStrain_smul (-1) H D
97
98theorem edgeStrain_sub (H K : Mat4) (D : Fin 4 → ℤ) :
99 edgeStrain (H - K) D = edgeStrain H D - edgeStrain K D := by
100 rw [sub_eq_add_neg, edgeStrain_add, edgeStrain_neg, ← sub_eq_add_neg]
101
102/-! ## §2. Cross-term first variation (genuine bilinearization) -/
103
104/-- Coupling weight cross term: polarization of the product of edge strains. -/
105def couplingWeightCross (H K : Mat4) (c : Coupling) : ℝ :=
106 (1 / 2 : ℝ) * (c.s : ℝ) *
107 (edgeStrain H c.De * edgeStrain K c.Dep +
108 edgeStrain K c.De * edgeStrain H c.Dep)
109
110def couplingWeightCrossIdx (H K : Mat4) (i : CouplingIdx) : ℝ :=
111 couplingWeightCross H K couplingTable[i]
112
113/-- Opaque cross-weight wrapper (Fin-1208 hygiene). -/
114irreducible_def crossWeightFn (H K : Mat4) : CouplingIdx → ℝ :=
115 couplingWeightCrossIdx H K
116
117/-- Directional first variation of `exactMidpointBlochSymbol` at `H` in
118direction `K` (finite coupling sum with cross edge-strain factors). -/
119def exactMidpointBlochFirstVariation (H K : Mat4) (k : Wave4) : ℝ :=
120 ∑ i : CouplingIdx,
121 couplingWeightCrossIdx H K i * Real.cos (couplingPhaseIdx k i)
122
123theorem exactMidpointBlochSymbol_eq_irred (H : Mat4) (k : Wave4) :
124 exactMidpointBlochSymbol H k =
125 ∑ i ∈ couplingUniv, weightFn H i * Real.cos (phaseFn k i) := by
126 rw [weightFn_def, phaseFn_def, couplingUniv_def]
127 rfl
128
129theorem exactMidpointBlochFirstVariation_eq_irred
130 (H K : Mat4) (k : Wave4) :
131 exactMidpointBlochFirstVariation H K k =
132 ∑ i ∈ couplingUniv,
133 crossWeightFn H K i * Real.cos (phaseFn k i) := by
134 rw [crossWeightFn_def, phaseFn_def, couplingUniv_def]
135 rfl
136
137theorem couplingWeight_line (H K : Mat4) (c : Coupling) (t : ℝ) :
138 couplingWeight (H + t • K) c =
139 couplingWeight H c +
140 t * couplingWeightCross H K c +
141 t ^ 2 * couplingWeight K c := by
142 unfold couplingWeight couplingWeightCross
143 have hDe :
144 edgeStrain (H + t • K) c.De =
145 edgeStrain H c.De + t * edgeStrain K c.De := by
146 rw [edgeStrain_add, edgeStrain_smul]
147 have hDep :
148 edgeStrain (H + t • K) c.Dep =
149 edgeStrain H c.Dep + t * edgeStrain K c.Dep := by
150 rw [edgeStrain_add, edgeStrain_smul]
151 rw [hDe, hDep]
152 ring
153
154theorem couplingWeightIdx_line (H K : Mat4) (i : CouplingIdx) (t : ℝ) :
155 couplingWeightIdx (H + t • K) i =
156 couplingWeightIdx H i +
157 t * couplingWeightCrossIdx H K i +
158 t ^ 2 * couplingWeightIdx K i := by
159 unfold couplingWeightIdx couplingWeightCrossIdx
160 exact couplingWeight_line H K couplingTable[i] t
161
162theorem weightFn_line (H K : Mat4) (t : ℝ) (i : CouplingIdx) :
163 weightFn (H + t • K) i =
164 weightFn H i + t * crossWeightFn H K i + t ^ 2 * weightFn K i := by
165 rw [weightFn_def, weightFn_def, weightFn_def, crossWeightFn_def]
166 exact couplingWeightIdx_line H K i t
167
168/-- Line expansion: `Q(H+tK) = Q(H) + t·FV(H,K) + t²·Q(K)`. -/
169theorem exactMidpointBlochSymbol_line (H K : Mat4) (k : Wave4) (t : ℝ) :
170 exactMidpointBlochSymbol (H + t • K) k =
171 exactMidpointBlochSymbol H k +
172 t * exactMidpointBlochFirstVariation H K k +
173 t ^ 2 * exactMidpointBlochSymbol K k := by
174 rw [exactMidpointBlochSymbol_eq_irred,
175 exactMidpointBlochSymbol_eq_irred H,
176 exactMidpointBlochSymbol_eq_irred K,
177 exactMidpointBlochFirstVariation_eq_irred]
178 have hsplit (i : CouplingIdx) (_ : i ∈ couplingUniv) :
179 weightFn (H + t • K) i * Real.cos (phaseFn k i) =
180 weightFn H i * Real.cos (phaseFn k i) +
181 t * (crossWeightFn H K i * Real.cos (phaseFn k i)) +
182 t ^ 2 * (weightFn K i * Real.cos (phaseFn k i)) := by
183 rw [weightFn_line]
184 ring
185 calc
186 ∑ i ∈ couplingUniv, weightFn (H + t • K) i * Real.cos (phaseFn k i)
187 = ∑ i ∈ couplingUniv,
188 (weightFn H i * Real.cos (phaseFn k i) +
189 t * (crossWeightFn H K i * Real.cos (phaseFn k i)) +
190 t ^ 2 * (weightFn K i * Real.cos (phaseFn k i))) :=
191 Finset.sum_congr rfl hsplit
192 _ = (∑ i ∈ couplingUniv, weightFn H i * Real.cos (phaseFn k i)) +
193 (∑ i ∈ couplingUniv,
194 t * (crossWeightFn H K i * Real.cos (phaseFn k i))) +
195 ∑ i ∈ couplingUniv,
196 t ^ 2 * (weightFn K i * Real.cos (phaseFn k i)) := by
197 rw [Finset.sum_add_distrib, Finset.sum_add_distrib]
198 _ = (∑ i ∈ couplingUniv, weightFn H i * Real.cos (phaseFn k i)) +
199 t * ∑ i ∈ couplingUniv,
200 crossWeightFn H K i * Real.cos (phaseFn k i) +
201 t ^ 2 *
202 ∑ i ∈ couplingUniv, weightFn K i * Real.cos (phaseFn k i) := by
203 rw [← Finset.mul_sum, ← Finset.mul_sum]
204
205private theorem hasDerivAt_affine_quad (a b c : ℝ) :
206 HasDerivAt (fun t : ℝ => a + b * t + c * t ^ 2) b 0 := by
207 have h1 : HasDerivAt (fun t : ℝ => t ^ 2) 0 0 := by
208 simpa using hasDerivAt_pow 2 (0 : ℝ)
209 have h2 : HasDerivAt (fun t : ℝ => c * t ^ 2) 0 0 := by
210 simpa using h1.const_mul c
211 have h3 : HasDerivAt (fun t : ℝ => b * t) b 0 := by
212 simpa using (hasDerivAt_id (0 : ℝ)).const_mul b
213 have h4 := (h2.add h3).add_const a
214 have hfun :
215 (fun t : ℝ => a + b * t + c * t ^ 2) =
216 fun x : ℝ =>
217 ((fun t : ℝ => c * t ^ 2) + (fun t : ℝ => b * t)) x + a := by
218 funext t
219 simp only [Pi.add_apply]
220 ring
221 rw [hfun]
222 simpa using h4
223
224/-- Finite-line directional derivative of the midpoint symbol at `t = 0`. -/
225theorem hasDerivAt_exactMidpointBlochSymbol_line
226 (H K : Mat4) (k : Wave4) :
227 HasDerivAt (fun t : ℝ => exactMidpointBlochSymbol (H + t • K) k)
228 (exactMidpointBlochFirstVariation H K k) 0 := by
229 have hfun :
230 (fun t : ℝ => exactMidpointBlochSymbol (H + t • K) k) =
231 fun t : ℝ =>
232 exactMidpointBlochSymbol H k +
233 exactMidpointBlochFirstVariation H K k * t +
234 exactMidpointBlochSymbol K k * t ^ 2 := by
235 funext t
236 simpa [mul_comm, add_assoc, add_left_comm, add_comm] using
237 exactMidpointBlochSymbol_line H K k t
238 rw [hfun]
239 exact hasDerivAt_affine_quad (exactMidpointBlochSymbol H k)
240 (exactMidpointBlochFirstVariation H K k) (exactMidpointBlochSymbol K k)
241
242/-- Polarization identity for the midpoint first variation. -/
243theorem exactMidpointBlochFirstVariation_polarization
244 (H K : Mat4) (k : Wave4) :
245 exactMidpointBlochFirstVariation H K k =
246 (exactMidpointBlochSymbol (H + K) k -
247 exactMidpointBlochSymbol (H - K) k) / 2 := by
248 have hPlus :
249 exactMidpointBlochSymbol (H + K) k =
250 exactMidpointBlochSymbol H k +
251 exactMidpointBlochFirstVariation H K k +
252 exactMidpointBlochSymbol K k := by
253 simpa [one_smul] using exactMidpointBlochSymbol_line H K k 1
254 have hMinus :
255 exactMidpointBlochSymbol (H - K) k =
256 exactMidpointBlochSymbol H k -
257 exactMidpointBlochFirstVariation H K k +
258 exactMidpointBlochSymbol K k := by
259 have h := exactMidpointBlochSymbol_line H K k (-1)
260 have hsmul : H + (-1 : ℝ) • K = H - K := by
261 rw [neg_one_smul, sub_eq_add_neg]
262 rw [hsmul] at h
263 -- Q(H-K) = Q(H) + (-1)·FV + ((-1)²)·Q(K)
264 linarith
265 linarith
266
267/-! ## §3. IsTT closed under add / sub -/
268
269theorem IsSymmetric_add {H K : Mat4}
270 (hH : IsSymmetric H) (hK : IsSymmetric K) : IsSymmetric (H + K) := by
271 intro i j
272 simp only [Matrix.add_apply, hH i j, hK i j]
273
274theorem IsSymmetric_sub {H K : Mat4}
275 (hH : IsSymmetric H) (hK : IsSymmetric K) : IsSymmetric (H - K) := by
276 intro i j
277 simp only [Matrix.sub_apply, hH i j, hK i j]
278
279theorem IsTraceless_add {H K : Mat4}
280 (hH : IsTraceless H) (hK : IsTraceless K) : IsTraceless (H + K) := by
281 unfold IsTraceless euclideanTrace at hH hK ⊢
282 simp only [Matrix.add_apply]
283 rw [Finset.sum_add_distrib, hH, hK, add_zero]
284
285theorem IsTraceless_sub {H K : Mat4}
286 (hH : IsTraceless H) (hK : IsTraceless K) : IsTraceless (H - K) := by
287 unfold IsTraceless euclideanTrace at hH hK ⊢
288 simp only [Matrix.sub_apply]
289 rw [Finset.sum_sub_distrib, hH, hK, sub_zero]
290
291theorem IsTransverse_add {m : Wave4} {H K : Mat4}
292 (hH : IsTransverse m H) (hK : IsTransverse m K) :
293 IsTransverse m (H + K) := by
294 intro i
295 simp only [Matrix.add_apply, add_mul]
296 rw [Finset.sum_add_distrib, hH i, hK i, add_zero]
297
298theorem IsTransverse_sub {m : Wave4} {H K : Mat4}
299 (hH : IsTransverse m H) (hK : IsTransverse m K) :
300 IsTransverse m (H - K) := by
301 intro i
302 simp only [Matrix.sub_apply, sub_mul]
303 rw [Finset.sum_sub_distrib, hH i, hK i, sub_zero]
304
305theorem IsTT_add {m : Wave4} {H K : Mat4}
306 (hH : IsTT m H) (hK : IsTT m K) : IsTT m (H + K) :=
307 ⟨IsSymmetric_add hH.1 hK.1, IsTraceless_add hH.2.1 hK.2.1,
308 IsTransverse_add hH.2.2 hK.2.2⟩
309
310theorem IsTT_sub {m : Wave4} {H K : Mat4}
311 (hH : IsTT m H) (hK : IsTT m K) : IsTT m (H - K) :=
312 ⟨IsSymmetric_sub hH.1 hK.1, IsTraceless_sub hH.2.1 hK.2.1,
313 IsTransverse_sub hH.2.2 hK.2.2⟩
314
315/-! ## §4. Continuum face polarization and TT first-variation Tendsto -/
316
317theorem frobeniusPairing4D_polarization (H K : Mat4) :
318 frobeniusNormSq (H + K) - frobeniusNormSq (H - K) =
319 4 * frobeniusPairing4D H K := by
320 unfold frobeniusNormSq frobeniusPairing4D
321 calc
322 (∑ i : Fin 4, ∑ j : Fin 4, (H + K) i j * (H + K) i j) -
323 ∑ i : Fin 4, ∑ j : Fin 4, (H - K) i j * (H - K) i j
324 = ∑ i : Fin 4,
325 (∑ j : Fin 4, (H + K) i j * (H + K) i j -
326 ∑ j : Fin 4, (H - K) i j * (H - K) i j) := by
327 rw [← Finset.sum_sub_distrib]
328 _ = ∑ i : Fin 4, ∑ j : Fin 4,
329 ((H + K) i j * (H + K) i j - (H - K) i j * (H - K) i j) := by
330 refine Finset.sum_congr rfl fun i _ => ?_
331 rw [← Finset.sum_sub_distrib]
332 _ = ∑ i : Fin 4, ∑ j : Fin 4, 4 * (H i j * K i j) := by
333 refine Finset.sum_congr rfl fun i _ =>
334 Finset.sum_congr rfl fun j _ => ?_
335 simp only [Matrix.add_apply, Matrix.sub_apply]
336 ring
337 _ = 4 * ∑ i : Fin 4, ∑ j : Fin 4, H i j * K i j := by
338 rw [Finset.mul_sum]
339 refine Finset.sum_congr rfl fun i _ =>
340 (Finset.mul_sum Finset.univ (fun j => H i j * K i j) 4).symm
341
342/-- Algebraic continuum-face polarization equals `-(1/4)` Frobenius pairing. -/
343theorem continuumFace_polarization_eq_neg_quarter_frobenius
344 (H K : Mat4) :
345 (continuumEHScaleExplicitFace (H + K) -
346 continuumEHScaleExplicitFace (H - K)) / 2 =
347 -(1 / 4 : ℝ) * frobeniusPairing4D H K := by
348 rw [continuumEHScaleExplicitFace_eq, continuumEHScaleExplicitFace_eq]
349 have h := frobeniusPairing4D_polarization H K
350 linarith
351
352theorem momentumNormSq_torus_ne_zero (j : ℕ) (m : IntMode4) (hm : m ≠ 0) :
353 momentumNormSq (torusSide j) m ≠ 0 := by
354 rw [momentumNormSq_eq_scale_sq]
355 have hscale : torusScale j ≠ 0 := by
356 unfold torusScale torusSide
357 have hN : ((j + 3 : ℕ) : ℝ) ≠ 0 :=
358 Nat.cast_ne_zero.mpr (by omega)
359 exact div_ne_zero (mul_ne_zero (by norm_num : (2 : ℝ) ≠ 0) Real.pi_ne_zero) hN
360 exact mul_ne_zero (pow_ne_zero 2 hscale) (waveNormSq_intMode_ne_zero m hm)
361
362/-- Normalized finite-mesh directional derivative (no continuum interchange). -/
363theorem hasDerivAt_finiteExactMidpointBlochSymbol_normalized
364 (j : ℕ) (m : IntMode4) (H K : Mat4) (hm : m ≠ 0) :
365 HasDerivAt
366 (fun t : ℝ =>
367 finiteExactMidpointBlochSymbol j m (H + t • K) /
368 momentumNormSq (torusSide j) m)
369 (exactMidpointBlochFirstVariation H K (realMode (torusSide j) m) /
370 momentumNormSq (torusSide j) m)
371 0 := by
372 have hn := momentumNormSq_torus_ne_zero j m hm
373 have h :=
374 hasDerivAt_exactMidpointBlochSymbol_line H K (realMode (torusSide j) m)
375 simpa [finiteExactMidpointBlochSymbol] using h.div_const _
376
377/-- **Headline THEOREM (Euclidean weak-field TT sector):** the torus-normalized
378midpoint first variation tends to `-(1/4)` Frobenius pairing. -/
379theorem continuumTTFirstVariation_closed :
380 ∀ (m : IntMode4) (H K : Mat4),
381 m ≠ 0 →
382 IsTT (fun i => (m i : ℝ)) H →
383 IsTT (fun i => (m i : ℝ)) K →
384 Tendsto
385 (fun j : ℕ =>
386 exactMidpointBlochFirstVariation H K
387 (realMode (torusSide j) m) /
388 momentumNormSq (torusSide j) m)
389 atTop
390 (nhds (-(1 / 4 : ℝ) * frobeniusPairing4D H K)) := by
391 intro m H K hm hH hK
392 have hTT_add : IsTT (fun i => (m i : ℝ)) (H + K) := IsTT_add hH hK
393 have hTT_sub : IsTT (fun i => (m i : ℝ)) (H - K) := IsTT_sub hH hK
394 have hPlus := S_RS_converges_EH_4d_closed.1 m (H + K) hm hTT_add
395 have hMinus := S_RS_converges_EH_4d_closed.1 m (H - K) hm hTT_sub
396 have hDiff := hPlus.sub hMinus
397 have hFace := continuumFace_polarization_eq_neg_quarter_frobenius H K
398 have hSeq :
399 (fun j : ℕ =>
400 (finiteExactMidpointBlochSymbol j m (H + K) /
401 momentumNormSq (torusSide j) m -
402 finiteExactMidpointBlochSymbol j m (H - K) /
403 momentumNormSq (torusSide j) m) /
404 2) =
405 fun j : ℕ =>
406 exactMidpointBlochFirstVariation H K (realMode (torusSide j) m) /
407 momentumNormSq (torusSide j) m := by
408 funext j
409 have hn := momentumNormSq_torus_ne_zero j m hm
410 have hpol :=
411 exactMidpointBlochFirstVariation_polarization H K
412 (realMode (torusSide j) m)
413 change
414 ((exactMidpointBlochSymbol (H + K) (realMode (torusSide j) m) /
415 momentumNormSq (torusSide j) m -
416 exactMidpointBlochSymbol (H - K) (realMode (torusSide j) m) /
417 momentumNormSq (torusSide j) m) /
418 2) =
419 exactMidpointBlochFirstVariation H K (realMode (torusSide j) m) /
420 momentumNormSq (torusSide j) m
421 field_simp [hn]
422 linarith [hpol]
423 have hTend :
424 Tendsto
425 (fun j : ℕ =>
426 (finiteExactMidpointBlochSymbol j m (H + K) /
427 momentumNormSq (torusSide j) m -
428 finiteExactMidpointBlochSymbol j m (H - K) /
429 momentumNormSq (torusSide j) m) /
430 2)
431 atTop
432 (nhds
433 ((continuumEHScaleExplicitFace (H + K) -
434 continuumEHScaleExplicitFace (H - K)) / 2)) :=
435 hDiff.div_const 2
436 have hTend' :
437 Tendsto
438 (fun j : ℕ =>
439 exactMidpointBlochFirstVariation H K (realMode (torusSide j) m) /
440 momentumNormSq (torusSide j) m)
441 atTop
442 (nhds
443 ((continuumEHScaleExplicitFace (H + K) -
444 continuumEHScaleExplicitFace (H - K)) / 2)) := by
445 rwa [hSeq] at hTend
446 simpa [hFace] using hTend'
447
448/-! ## §5. Packaged certificate -/
449
450/-- Bundle: line derivative, polarization identity, continuum TT theorem. -/
451def SRSTTFirstVariation4DCert : Prop :=
452 (∀ (H K : Mat4) (k : Wave4),
453 HasDerivAt (fun t : ℝ => exactMidpointBlochSymbol (H + t • K) k)
454 (exactMidpointBlochFirstVariation H K k) 0) ∧
455 (∀ (H K : Mat4) (k : Wave4),
456 exactMidpointBlochFirstVariation H K k =
457 (exactMidpointBlochSymbol (H + K) k -
458 exactMidpointBlochSymbol (H - K) k) / 2) ∧
459 (∀ (m : IntMode4) (H K : Mat4),
460 m ≠ 0 →
461 IsTT (fun i => (m i : ℝ)) H →
462 IsTT (fun i => (m i : ℝ)) K →
463 Tendsto
464 (fun j : ℕ =>
465 exactMidpointBlochFirstVariation H K
466 (realMode (torusSide j) m) /
467 momentumNormSq (torusSide j) m)
468 atTop
469 (nhds (-(1 / 4 : ℝ) * frobeniusPairing4D H K)))
470
471theorem srsTTFirstVariation4D_cert : SRSTTFirstVariation4DCert :=
472 ⟨hasDerivAt_exactMidpointBlochSymbol_line,
473 exactMidpointBlochFirstVariation_polarization,
474 continuumTTFirstVariation_closed⟩
475
476end
477
478end SRSTTFirstVariation4D
479end Analysis
480end Gravity
481end IndisputableMonolith
482