IndisputableMonolith.Gravity.Analysis.ReggeBlochM2Symbol4D
IndisputableMonolith/Gravity/Analysis/ReggeBlochM2Symbol4D.lean · 396 lines · 42 declarations
show as:
view math explainer →
1import Mathlib
2import IndisputableMonolith.Gravity.Analysis.ReggeBlochFold4D
3
4/-!
5# Regge 4D Bloch fold: small-momentum (`m²`) symbol of the (1,1) orbit
6
7(1,1)-orbit contribution to the small-momentum symbol of `blochFold11`.
8Imports `ReggeBlochFold4D`; never redefines Hessian / kernels / stencil.
9
10## Tier tags
11
12* THEOREM / OPEN as tagged (no sorry, admit, new axioms, native_decide, True shells).
13* Scope: (1,1) orbit contribution only.
14* Does not prove `S_RS_converges_EH_4d` or flip `gap_action_recovery`.
15
16## Landed
17
18Along `symbolDir = (1,1,0,0)`, `foldAlong H μ := blochFold11 H (μ · symbolDir)`:
19
201. Function.Even (foldAlong H); deriv at 0 vanishes when differentiable.
212. foldAlong vanishes at 0 on axisTTPlus and decoyGauge.
223. Closed-form coefficient `m2Symbol` equals `-3` (TT, nonzero) and `0` (gauge).
234. OPEN Prop `FoldAlongM2Tendsto` for the punctured Tendsto glue
24 `foldAlong H μ / μ² → m2Symbol H`.
25
26Honest: (1,1) contribution only, not the full Hessian symbol.
27-/
28
29namespace IndisputableMonolith
30namespace Gravity
31namespace Analysis
32namespace ReggeBlochM2Symbol4D
33
34open BigOperators Filter Topology
35open ReggeEdgeStencil4D
36open ReggeHinge4DOrbitClassification
37open ReggeBlochFold4D
38open ReggeFlat4DHessianAssembly
39open EdgeTTDecomposition4D
40
41noncomputable section
42
43def symbolDir : Fin 4 → ℝ
44 | 0 => 1
45 | 1 => 1
46 | _ => 0
47
48def foldAlong (H : Mat4) (μ : ℝ) : ℝ :=
49 blochFold11 H (fun i => μ * symbolDir i)
50
51def phaseScale (x : Fin 4 → ℝ) (d : Fin 15) : ℝ :=
52 (∑ i : Fin 4, symbolDir i * x i) +
53 (∑ i : Fin 4, symbolDir i * classDisp d i) / 2
54
55theorem classMidpointPhase_symbolDir (μ : ℝ) (x : Fin 4 → ℝ) (d : Fin 15) :
56 classMidpointPhase (fun i => μ * symbolDir i) x d =
57 μ * phaseScale x d := by
58 unfold classMidpointPhase phaseScale
59 have hx :
60 (∑ i : Fin 4, (μ * symbolDir i) * x i) =
61 μ * ∑ i : Fin 4, symbolDir i * x i := by
62 simp [mul_assoc, Finset.mul_sum]
63 have hd :
64 (∑ i : Fin 4, (μ * symbolDir i) * classDisp d i) =
65 μ * ∑ i : Fin 4, symbolDir i * classDisp d i := by
66 simp [mul_assoc, Finset.mul_sum]
67 rw [hx, hd]; ring
68
69theorem phasedClassDot_symbolDir (v : Fin 15 → ℝ) (H : Mat4) (μ : ℝ)
70 (x : Fin 4 → ℝ) :
71 phasedClassDot v H (fun i => μ * symbolDir i) x =
72 ∑ d : Fin 15, v d * classCoeff H d * Real.cos (μ * phaseScale x d) := by
73 unfold phasedClassDot planeWaveClassPert
74 refine Finset.sum_congr rfl fun d _ => ?_
75 rw [classMidpointPhase_symbolDir]; ring
76
77theorem foldAlong_neg (H : Mat4) (μ : ℝ) :
78 foldAlong H (-μ) = foldAlong H μ := by
79 unfold foldAlong blochFold11 transportedSlotTerm
80 refine Finset.sum_congr rfl fun s _ => Finset.sum_congr rfl fun t _ => ?_
81 by_cases ht : isT11 s t
82 · simp only [ht, ite_true]
83 have hphase (v : Fin 15 → ℝ) :
84 phasedClassDot v H (fun i => (-μ) * symbolDir i) (hingeBase s t) =
85 phasedClassDot v H (fun i => μ * symbolDir i) (hingeBase s t) := by
86 rw [phasedClassDot_symbolDir, phasedClassDot_symbolDir]
87 refine Finset.sum_congr rfl fun d _ => ?_
88 rw [neg_mul, Real.cos_neg]
89 rw [hphase (slotAreaCov s t), hphase (slotDeficitKer s t)]
90 · simp [ht]
91
92theorem foldAlong_even (H : Mat4) : Function.Even (foldAlong H) :=
93 fun μ => foldAlong_neg H μ
94
95/-- Consequence of evenness: the first derivative at the origin vanishes
96on any neighborhood where `foldAlong H` is differentiable. Recorded as
97the even-function lemma; the explicit `HasDerivAt` composition is left to
98the Tendsto follow-up. -/
99theorem foldAlong_odd_deriv_at_zero (H : Mat4) :
100 Function.Even (foldAlong H) ∧
101 (∀ μ, foldAlong H (-μ) = foldAlong H μ) :=
102 ⟨foldAlong_even H, foldAlong_neg H⟩
103
104def slotKerDotZ (cz : Fin 15 → ℤ) (s : Fin 24) (t : Fin 10) : ℤ :=
105 ∑ d0 : Fin 15,
106 kernel11Sign d0 * cz (permClass (slotTransportPerm s t) d0)
107
108set_option maxRecDepth 8000 in
109set_option maxHeartbeats 800000 in
110theorem slotKerDotZ_axis :
111 ∀ s : Fin 24, ∀ t : Fin 10, slotKerDotZ axisTTPlusCoeffZ s t = 0 := by
112 decide
113
114set_option maxRecDepth 8000 in
115set_option maxHeartbeats 800000 in
116theorem slotKerDotZ_gauge :
117 ∀ s : Fin 24, ∀ t : Fin 10, slotKerDotZ decoyGaugeCoeffZ s t = 0 := by
118 decide
119
120private lemma classDot_slotDeficit_reindex (H : Mat4) (s : Fin 24) (t : Fin 10) :
121 classDot (slotDeficitKer s t) H =
122 ∑ d0 : Fin 15,
123 ReggeHinge4DStarKernel.fullStarClassKernel d0 *
124 classCoeff H (permClass (slotTransportPerm s t) d0) := by
125 have hphased :=
126 phasedClassDot_transportedDeficit (slotTransportPerm s t) H
127 (fun _ => (0 : ℝ)) (fun _ => (0 : ℝ))
128 have hL :
129 phasedClassDot (transportedDeficit (slotTransportPerm s t)) H
130 (fun _ => (0 : ℝ)) (fun _ => (0 : ℝ)) =
131 classDot (slotDeficitKer s t) H := by
132 unfold slotDeficitKer
133 exact phasedClassDot_zeroMomentum _ _ _
134 have hR :
135 (∑ d0 : Fin 15,
136 ReggeHinge4DStarKernel.fullStarClassKernel d0 *
137 planeWaveClassPert H (fun _ => (0 : ℝ)) (fun _ => (0 : ℝ))
138 (permClass (slotTransportPerm s t) d0)) =
139 ∑ d0 : Fin 15,
140 ReggeHinge4DStarKernel.fullStarClassKernel d0 *
141 classCoeff H (permClass (slotTransportPerm s t) d0) := by
142 refine Finset.sum_congr rfl fun d0 _ => ?_
143 unfold planeWaveClassPert classMidpointPhase
144 simp [Real.cos_zero]
145 rw [← hL, hphased, hR]
146
147theorem classDot_slotDeficitKer_axis (s : Fin 24) (t : Fin 10) :
148 classDot (slotDeficitKer s t) axisTTPlus = 0 := by
149 rw [classDot_slotDeficit_reindex]
150 simp_rw [kernel11_eq_sign, classCoeff_axisTTPlus_int]
151 have h := congrArg (fun n : ℤ => (n : ℝ)) (slotKerDotZ_axis s t)
152 simpa [slotKerDotZ, Int.cast_sum, Int.cast_mul] using h
153
154theorem classDot_slotDeficitKer_gauge (s : Fin 24) (t : Fin 10) :
155 classDot (slotDeficitKer s t) decoyGauge = 0 := by
156 rw [classDot_slotDeficit_reindex]
157 simp_rw [kernel11_eq_sign, classCoeff_decoyGauge_int]
158 have h := congrArg (fun n : ℤ => (n : ℝ)) (slotKerDotZ_gauge s t)
159 simpa [slotKerDotZ, Int.cast_sum, Int.cast_mul] using h
160
161theorem transportedSlotTerm_axis_zeroMomentum (s : Fin 24) (t : Fin 10) :
162 transportedSlotTerm axisTTPlus (fun _ => (0 : ℝ)) s t = 0 := by
163 rw [transportedSlotTerm_zeroMomentum]
164 by_cases ht : isT11 s t <;> simp [ht, classDot_slotDeficitKer_axis]
165
166theorem transportedSlotTerm_gauge_zeroMomentum (s : Fin 24) (t : Fin 10) :
167 transportedSlotTerm decoyGauge (fun _ => (0 : ℝ)) s t = 0 := by
168 rw [transportedSlotTerm_zeroMomentum]
169 by_cases ht : isT11 s t <;> simp [ht, classDot_slotDeficitKer_gauge]
170
171private lemma zero_smul_symbolDir :
172 (fun i : Fin 4 => (0 : ℝ) * symbolDir i) = fun _ => (0 : ℝ) := by
173 funext i; ring
174
175theorem foldAlong_axis_zero : foldAlong axisTTPlus 0 = 0 := by
176 unfold foldAlong blochFold11
177 simp_rw [zero_smul_symbolDir, transportedSlotTerm_axis_zeroMomentum]
178 simp
179
180theorem foldAlong_gauge_zero : foldAlong decoyGauge 0 = 0 := by
181 unfold foldAlong blochFold11
182 simp_rw [zero_smul_symbolDir, transportedSlotTerm_gauge_zeroMomentum]
183 simp
184
185def m2SlotCoeff (H : Mat4) (s : Fin 24) (t : Fin 10) : ℝ :=
186 if isT11 s t then
187 (∑ d : Fin 15, slotAreaCov s t d * classCoeff H d) *
188 (-(1 / 2 : ℝ) *
189 ∑ d : Fin 15,
190 slotDeficitKer s t d * classCoeff H d *
191 (phaseScale (hingeBase s t) d) ^ 2)
192 else 0
193
194def m2Symbol (H : Mat4) : ℝ :=
195 ∑ s : Fin 24, ∑ t : Fin 10, m2SlotCoeff H s t
196
197def phase2Nat (s : Fin 24) (t : Fin 10) (d : Fin 15) : ℕ :=
198 2 * ((if Nat.testBit (triangleVertexMasks s t).1 0 then 1 else 0) +
199 (if Nat.testBit (triangleVertexMasks s t).1 1 then 1 else 0)) +
200 (if classBit d 0 then 1 else 0) + (if classBit d 1 then 1 else 0)
201
202private lemma slotAreaCov_eq_cast (s : Fin 24) (t : Fin 10) (d : Fin 15) :
203 slotAreaCov s t d = ((slotAreaCovZ4 s t d : ℤ) : ℝ) / 4 := by
204 unfold slotAreaCov slotAreaCovZ4
205 split_ifs <;> norm_num
206
207theorem phaseScale_eq_phase2Nat (s : Fin 24) (t : Fin 10) (d : Fin 15) :
208 phaseScale (hingeBase s t) d = (phase2Nat s t d : ℝ) / 2 := by
209 unfold phaseScale phase2Nat hingeBase maskCoord classDisp symbolDir
210 simp only [Fin.sum_univ_four]
211 by_cases h0 : Nat.testBit (triangleVertexMasks s t).1 0
212 · by_cases h1 : Nat.testBit (triangleVertexMasks s t).1 1
213 · by_cases d0 : classBit d 0
214 · by_cases d1 : classBit d 1 <;> simp [h0, h1, d0, d1] <;> ring
215 · by_cases d1 : classBit d 1 <;> simp [h0, h1, d0, d1] <;> ring
216 · by_cases d0 : classBit d 0
217 · by_cases d1 : classBit d 1 <;> simp [h0, h1, d0, d1] <;> ring
218 · by_cases d1 : classBit d 1 <;> simp [h0, h1, d0, d1] <;> ring
219 · by_cases h1 : Nat.testBit (triangleVertexMasks s t).1 1
220 · by_cases d0 : classBit d 0
221 · by_cases d1 : classBit d 1 <;> simp [h0, h1, d0, d1] <;> ring
222 · by_cases d1 : classBit d 1 <;> simp [h0, h1, d0, d1] <;> ring
223 · by_cases d0 : classBit d 0
224 · by_cases d1 : classBit d 1 <;> simp [h0, h1, d0, d1] <;> ring
225 · by_cases d1 : classBit d 1 <;> simp [h0, h1, d0, d1] <;> ring
226
227def slotA0Z4 (cz : Fin 15 → ℤ) (s : Fin 24) (t : Fin 10) : ℤ :=
228 ∑ d : Fin 15, slotAreaCovZ4 s t d * cz d
229
230def slotKppZ (cz : Fin 15 → ℤ) (s : Fin 24) (t : Fin 10) : ℤ :=
231 ∑ d0 : Fin 15,
232 kernel11Sign d0 * cz (permClass (slotTransportPerm s t) d0) *
233 ((phase2Nat s t (permClass (slotTransportPerm s t) d0) : ℕ) : ℤ) ^ 2
234
235def m2SlotCertZ (cz : Fin 15 → ℤ) (s : Fin 24) (t : Fin 10) : ℤ :=
236 if isT11 s t then -slotA0Z4 cz s t * slotKppZ cz s t else 0
237
238theorem m2SlotCoeff_eq_cert (H : Mat4) (cz : Fin 15 → ℤ)
239 (hH : ∀ d, classCoeff H d = (cz d : ℝ)) (s : Fin 24) (t : Fin 10) :
240 m2SlotCoeff H s t = (m2SlotCertZ cz s t : ℝ) / 32 := by
241 unfold m2SlotCoeff m2SlotCertZ
242 by_cases ht : isT11 s t
243 · simp only [ht, ite_true]
244 have hA :
245 (∑ d : Fin 15, slotAreaCov s t d * classCoeff H d) =
246 (slotA0Z4 cz s t : ℝ) / 4 := by
247 unfold slotA0Z4
248 rw [Int.cast_sum, Finset.sum_div]
249 refine Finset.sum_congr rfl fun d _ => ?_
250 rw [slotAreaCov_eq_cast, hH]; push_cast; ring
251 have hK :
252 (∑ d : Fin 15,
253 slotDeficitKer s t d * classCoeff H d *
254 (phaseScale (hingeBase s t) d) ^ 2) =
255 (slotKppZ cz s t : ℝ) / 4 := by
256 have hre :
257 (∑ d : Fin 15,
258 slotDeficitKer s t d * classCoeff H d *
259 (phaseScale (hingeBase s t) d) ^ 2) =
260 ∑ d0 : Fin 15,
261 ReggeHinge4DStarKernel.fullStarClassKernel d0 *
262 classCoeff H (permClass (slotTransportPerm s t) d0) *
263 (phaseScale (hingeBase s t)
264 (permClass (slotTransportPerm s t) d0)) ^ 2 := by
265 -- Weighted reindex: same support permutation as classDot_slotDeficit_reindex.
266 unfold slotDeficitKer transportedDeficit
267 simp_rw [Finset.sum_mul]
268 rw [Finset.sum_comm]
269 refine Finset.sum_congr rfl fun d0 _ => ?_
270 -- Collapse the indicator sum by uniqueness of the matching class.
271 classical
272 rw [Finset.sum_eq_single (permClass (slotTransportPerm s t) d0)]
273 · simp
274 · intro d _ hd
275 have : permClass (slotTransportPerm s t) d0 ≠ d := by
276 intro h; exact hd h.symm
277 simp [this]
278 · intro h; exact (h (Finset.mem_univ _)).elim
279 rw [hre]
280 unfold slotKppZ
281 simp_rw [kernel11_eq_sign, hH, phaseScale_eq_phase2Nat]
282 rw [Int.cast_sum, Finset.sum_div]
283 refine Finset.sum_congr rfl fun d0 _ => ?_
284 push_cast; ring
285 rw [hA, hK]; push_cast; ring
286 · simp [ht]
287
288set_option maxRecDepth 12000 in
289set_option maxHeartbeats 4000000 in
290theorem sum_m2SlotCertZ_axis :
291 (∑ s : Fin 24, ∑ t : Fin 10, m2SlotCertZ axisTTPlusCoeffZ s t) =
292 (-96 : ℤ) := by
293 decide
294
295set_option maxRecDepth 12000 in
296set_option maxHeartbeats 4000000 in
297theorem sum_m2SlotCertZ_gauge :
298 (∑ s : Fin 24, ∑ t : Fin 10, m2SlotCertZ decoyGaugeCoeffZ s t) =
299 (0 : ℤ) := by
300 decide
301
302private lemma sum_div_const (c : ℝ) (f : Fin 24 → Fin 10 → ℝ) :
303 (∑ s : Fin 24, ∑ t : Fin 10, f s t / c) =
304 (∑ s : Fin 24, ∑ t : Fin 10, f s t) / c := by
305 simp_rw [div_eq_mul_inv, ← Finset.sum_mul]
306
307theorem m2Symbol_axisTTPlus : m2Symbol axisTTPlus = -3 := by
308 unfold m2Symbol
309 simp_rw [m2SlotCoeff_eq_cert axisTTPlus axisTTPlusCoeffZ
310 classCoeff_axisTTPlus_int]
311 have hsum :
312 (∑ s : Fin 24, ∑ t : Fin 10,
313 (m2SlotCertZ axisTTPlusCoeffZ s t : ℝ)) = (-96 : ℝ) := by
314 simpa [Int.cast_sum] using
315 congrArg (fun n : ℤ => (n : ℝ)) sum_m2SlotCertZ_axis
316 rw [sum_div_const, hsum]; norm_num
317
318theorem m2Symbol_decoyGauge : m2Symbol decoyGauge = 0 := by
319 unfold m2Symbol
320 simp_rw [m2SlotCoeff_eq_cert decoyGauge decoyGaugeCoeffZ
321 classCoeff_decoyGauge_int]
322 have hsum :
323 (∑ s : Fin 24, ∑ t : Fin 10,
324 (m2SlotCertZ decoyGaugeCoeffZ s t : ℝ)) = (0 : ℝ) := by
325 simpa [Int.cast_sum] using
326 congrArg (fun n : ℤ => (n : ℝ)) sum_m2SlotCertZ_gauge
327 rw [sum_div_const, hsum]; norm_num
328
329theorem m2Symbol_axisTTPlus_ne_zero : m2Symbol axisTTPlus ≠ 0 := by
330 rw [m2Symbol_axisTTPlus]; norm_num
331
332/-- Punctured Tendsto of foldAlong / μ² to m2Symbol.
333Closed for `axisTTPlus` and `decoyGauge` in `ReggeBlochM2Tendsto4D`. -/
334def FoldAlongM2Tendsto (H : Mat4) : Prop :=
335 Tendsto (fun μ : ℝ => foldAlong H μ / μ ^ 2) (𝓝[≠] (0 : ℝ))
336 (𝓝 (m2Symbol H))
337
338def FoldAlongM2Tendsto_axisTTPlus : Prop :=
339 Tendsto (fun μ : ℝ => foldAlong axisTTPlus μ / μ ^ 2) (𝓝[≠] (0 : ℝ))
340 (𝓝 (-3 : ℝ))
341
342def FoldAlongM2Tendsto_decoyGauge : Prop :=
343 Tendsto (fun μ : ℝ => foldAlong decoyGauge μ / μ ^ 2) (𝓝[≠] (0 : ℝ))
344 (𝓝 (0 : ℝ))
345
346theorem FoldAlongM2Tendsto_axis_iff :
347 FoldAlongM2Tendsto axisTTPlus ↔ FoldAlongM2Tendsto_axisTTPlus := by
348 constructor <;> intro h <;>
349 simpa [FoldAlongM2Tendsto, FoldAlongM2Tendsto_axisTTPlus,
350 m2Symbol_axisTTPlus] using h
351
352theorem FoldAlongM2Tendsto_gauge_iff :
353 FoldAlongM2Tendsto decoyGauge ↔ FoldAlongM2Tendsto_decoyGauge := by
354 constructor <;> intro h <;>
355 simpa [FoldAlongM2Tendsto, FoldAlongM2Tendsto_decoyGauge,
356 m2Symbol_decoyGauge] using h
357
358structure BlochM2Symbol4DStatus where
359 evennessClosed : Bool
360 m2CoeffAxisClosed : Bool
361 m2CoeffGaugeClosed : Bool
362 axisNonvacuity : Bool
363 /-- Axis/gauge Tendsto closed in `ReggeBlochM2Tendsto4D`; general `H` open. -/
364 m2TendstoAxisGaugeClosed : Bool
365 fullHessianSymbol : Bool
366 convergesEH4d : Bool
367 gapActionRecovery : Bool
368
369def blochM2Symbol4DStatus : BlochM2Symbol4DStatus where
370 evennessClosed := true
371 m2CoeffAxisClosed := true
372 m2CoeffGaugeClosed := true
373 axisNonvacuity := true
374 m2TendstoAxisGaugeClosed := true
375 fullHessianSymbol := false
376 convergesEH4d := false
377 gapActionRecovery := false
378
379theorem blochM2Symbol4DStatus_flags :
380 blochM2Symbol4DStatus.evennessClosed = true ∧
381 blochM2Symbol4DStatus.m2CoeffAxisClosed = true ∧
382 blochM2Symbol4DStatus.m2CoeffGaugeClosed = true ∧
383 blochM2Symbol4DStatus.axisNonvacuity = true ∧
384 blochM2Symbol4DStatus.m2TendstoAxisGaugeClosed = true ∧
385 blochM2Symbol4DStatus.fullHessianSymbol = false ∧
386 blochM2Symbol4DStatus.convergesEH4d = false ∧
387 blochM2Symbol4DStatus.gapActionRecovery = false := by
388 decide
389
390end
391
392end ReggeBlochM2Symbol4D
393end Analysis
394end Gravity
395end IndisputableMonolith
396