IndisputableMonolith.Gravity.Analysis.ReggeTTContinuumLimit
IndisputableMonolith/Gravity/Analysis/ReggeTTContinuumLimit.lean · 362 lines · 18 declarations
show as:
view math explainer →
1import IndisputableMonolith.Gravity.Analysis.ReggeTTBlochAssembly
2
3/-!
4# Regge TT cosine two-jet continuum limit
5
6This module is the C-DAG2 continuum stage. It imports the finite Bloch
7assembly and no continuum-certificate spike. Exact Bloch orthogonality has
8already removed the cell sum, so the proof is a local cosine two-jet limit of
9the finite raw bucket fold.
10
11The reusable theorem `rawCosineFold_scale_tendsto` treats a free real scale
12`q`. Its phase is literally `q * sum_i x_i * (u_i / 2)`, preserving the
13doubled-midpoint convention. The constant term is removed by the assembled
14zero-mode theorem, and the local centered-second-difference bridge supplies
15the cosine second jet. The final theorem composes this result with
16`q_N = 2*pi/N`, the eventual finite assembly theorem, and the exact
17`momentumNormSq` normalization.
18-/
19
20namespace IndisputableMonolith
21namespace Gravity
22namespace Analysis
23namespace ReggeTTContinuumLimit
24
25open ReggeTTSymbolPreflight
26open ReggeTTBlochInterfaceAudit
27open ReggeTTBlochAssembly
28open ReggeTTHingeAwareZeroMode
29
30noncomputable section
31
32/-- Literal midpoint-displacement phase `sum_i x_i * (u_i / 2)`. -/
33def rawPhaseLinear (x : Fin 3 → ℝ) (b : Bucket) : ℝ :=
34 ∑ i : Fin 3, x i * (((b.phase i : ℤ) : ℝ) / 2)
35
36/-- Frozen phase quadratic, with the literal doubled-key normalization
37`(sum_i x_i * (u_i / 2))^2`. -/
38def rawPhaseQuadratic (x : Fin 3 → ℝ) (b : Bucket) : ℝ :=
39 rawPhaseLinear x b ^ (2 : ℕ)
40
41/-- Raw cosine evaluator at a free continuous momentum scale `q`. -/
42def rawCosineEvaluatorAtScale (q : ℝ) (x : Fin 3 → ℝ) (b : Bucket) : ℝ :=
43 Real.cos (q * rawPhaseLinear x b)
44
45/-- The finite raw bucket fold at continuous scale `q`. -/
46def rawCosineFoldAtScale (q : ℝ) (x : Fin 3 → ℝ)
47 (E : Fin 3 → Fin 3 → ℝ) : ℝ :=
48 reggeTTBlochFold rawCosineSupport (rawCosineEvaluatorAtScale q x)
49 (rawBucketAmplitude E)
50
51/-- Squared Euclidean norm of a real mode direction. -/
52def realModeNormSq (x : Fin 3 → ℝ) : ℝ :=
53 ∑ i : Fin 3, x i ^ (2 : ℕ)
54
55/-- Real direction of an integer mode, normalized to unit Euclidean norm. -/
56def normalizedRealMode (m : Fin 3 → ℤ) : Fin 3 → ℝ :=
57 fun i => (m i : ℝ) / Real.sqrt (realModeNormSq (fun j => (m j : ℝ)))
58
59/-- The continuous scale used by the side-`N` commensurate momentum. -/
60def sideScale (N : ℕ) : ℝ :=
61 2 * Real.pi / (N : ℝ)
62
63/-- The scale-zero raw cosine fold is the assembled constant block and hence
64vanishes. This consumes the hinge-aware assembled zero-mode theorem, not a
65stencil-only cancellation. -/
66theorem rawCosineFoldAtScale_zero (x : Fin 3 → ℝ)
67 (E : Fin 3 → Fin 3 → ℝ) :
68 rawCosineFoldAtScale 0 x E = 0 := by
69 have hfold :=
70 rawCosineFold_eq_rawTripleSum (N := 1) E (fun _ => (0 : ℤ))
71 have heval :
72 rawCosineFoldAtScale 0 x E =
73 reggeTTBlochFold rawCosineSupport
74 (@rawCosineEvaluator 1 (by infer_instance) (fun _ => (0 : ℤ)))
75 (rawBucketAmplitude E) := by
76 unfold rawCosineFoldAtScale reggeTTBlochFold
77 refine Finset.sum_congr rfl fun b _ => ?_
78 simp [rawCosineEvaluatorAtScale, rawPhaseLinear, rawCosineEvaluator,
79 commensurateMomentum]
80 rw [heval, hfold]
81 have hone : ∀ p : Fin 6 × Fin 6 × Fin 6,
82 rawCosineEvaluator 1 (fun _ => (0 : ℤ)) (bucketKeyOf p) = 1 := by
83 intro p
84 unfold rawCosineEvaluator commensurateMomentum
85 norm_num
86 have hsum :
87 (∑ p : Fin 6 × Fin 6 × Fin 6,
88 rawCosineEvaluator 1 (fun _ => (0 : ℤ)) (bucketKeyOf p) *
89 rawTripleWeight E p) = assembledConstantBlock E := by
90 unfold assembledConstantBlock rawTripleWeight
91 rw [Fintype.sum_prod_type]
92 simp_rw [Fintype.sum_prod_type, hone, one_mul, Finset.sum_neg_distrib]
93 rw [hsum]
94 exact assembledConstantBlock_eq_zero E
95
96/-- The second derivative at zero of `q ↦ cos(aq)` is `-a^2`. -/
97theorem iteratedDeriv_two_cos_mul (a : ℝ) :
98 iteratedDeriv 2 (fun q : ℝ => Real.cos (a * q)) 0 = -(a ^ (2 : ℕ)) := by
99 have hinner : ∀ q : ℝ, HasDerivAt (fun s : ℝ => a * s) a q := by
100 intro q
101 simpa using (hasDerivAt_id q).const_mul a
102 have hfirst :
103 deriv (fun q : ℝ => Real.cos (a * q)) =
104 fun q : ℝ => -Real.sin (a * q) * a := by
105 funext q
106 exact ((Real.hasDerivAt_cos (a * q)).comp q (hinner q)).deriv
107 rw [show (2 : ℕ) = 1 + 1 from rfl, iteratedDeriv_succ,
108 iteratedDeriv_one, hfirst]
109 have hsecond :
110 HasDerivAt (fun q : ℝ => -Real.sin (a * q) * a)
111 (-Real.cos (a * 0) * a * a) 0 := by
112 have h :=
113 ((Real.hasDerivAt_sin (a * 0)).comp 0 (hinner 0)).neg.mul_const a
114 simpa [Function.comp, neg_mul] using h
115 rw [hsecond.deriv]
116 simp [Real.cos_zero]
117 ring
118
119/-- Local cosine two-jet obtained from the reusable centered-second-difference
120theorem of the finite-symbol existence stage. -/
121theorem cos_sub_one_div_sq_tendsto (a : ℝ) :
122 Filter.Tendsto
123 (fun q : ℝ => (Real.cos (q * a) - 1) / q ^ (2 : ℕ))
124 (nhdsWithin 0 {(0 : ℝ)}ᶜ) (nhds (-(a ^ (2 : ℕ)) / 2)) := by
125 have hC2 : ContDiffAt ℝ 2 (fun q : ℝ => Real.cos (a * q)) 0 :=
126 (Real.contDiff_cos.comp (contDiff_const.mul contDiff_id)).contDiffAt
127 have hcenter :=
128 ReggeTTLocalSymbolExistence.tendsto_centeredSecondDifference_of_contDiffAt
129 (fun q : ℝ => Real.cos (a * q)) hC2
130 rw [iteratedDeriv_two_cos_mul a] at hcenter
131 have hhalf := hcenter.const_mul (1 / 2 : ℝ)
132 have heq :
133 (fun q : ℝ => (Real.cos (q * a) - 1) / q ^ (2 : ℕ)) =
134 fun t : ℝ =>
135 1 / 2 *
136 (((fun q : ℝ => Real.cos (a * q)) t -
137 2 * (fun q : ℝ => Real.cos (a * q)) 0 +
138 (fun q : ℝ => Real.cos (a * q)) (-t)) / t ^ (2 : ℕ)) := by
139 funext t
140 simp only [mul_zero, Real.cos_zero, mul_neg, Real.cos_neg, mul_comm t a]
141 ring
142 rw [heq, show -(a ^ (2 : ℕ)) / 2 = 1 / 2 * -(a ^ (2 : ℕ)) by ring]
143 exact hhalf
144
145/-- REUSABLE CONTINUOUS-VARIABLE HEADLINE: after assembled zero-mode
146cancellation, the finite raw cosine fold divided by `q^2` tends exactly to
147`reggeTTMoment` with the literal midpoint phase quadratic. -/
148theorem rawCosineFold_scale_tendsto (x : Fin 3 → ℝ)
149 (E : Fin 3 → Fin 3 → ℝ) :
150 Filter.Tendsto
151 (fun q : ℝ => rawCosineFoldAtScale q x E / q ^ (2 : ℕ))
152 (nhdsWithin 0 {(0 : ℝ)}ᶜ)
153 (nhds
154 (reggeTTMoment rawCosineSupport (rawPhaseQuadratic x)
155 (rawBucketAmplitude E))) := by
156 have hzero := rawCosineFoldAtScale_zero x E
157 have hsum :
158 Filter.Tendsto
159 (fun q : ℝ =>
160 ∑ b ∈ rawCosineSupport,
161 ((Real.cos (q * rawPhaseLinear x b) - 1) / q ^ (2 : ℕ)) *
162 rawBucketAmplitude E b)
163 (nhdsWithin 0 {(0 : ℝ)}ᶜ)
164 (nhds
165 (∑ b ∈ rawCosineSupport,
166 (-(rawPhaseLinear x b ^ (2 : ℕ)) / 2) *
167 rawBucketAmplitude E b)) := by
168 apply tendsto_finset_sum
169 intro b _
170 exact (cos_sub_one_div_sq_tendsto (rawPhaseLinear x b)).mul_const
171 (rawBucketAmplitude E b)
172 have hcongr :
173 (fun q : ℝ => rawCosineFoldAtScale q x E / q ^ (2 : ℕ)) =ᶠ[
174 nhdsWithin 0 {(0 : ℝ)}ᶜ]
175 (fun q : ℝ =>
176 ∑ b ∈ rawCosineSupport,
177 ((Real.cos (q * rawPhaseLinear x b) - 1) / q ^ (2 : ℕ)) *
178 rawBucketAmplitude E b) := by
179 filter_upwards [self_mem_nhdsWithin] with q hq
180 unfold rawCosineFoldAtScale reggeTTBlochFold
181 have hzero' :
182 ∑ b ∈ rawCosineSupport, rawBucketAmplitude E b = 0 := by
183 simpa [rawCosineFoldAtScale, reggeTTBlochFold,
184 rawCosineEvaluatorAtScale] using hzero
185 calc
186 (∑ b ∈ rawCosineSupport,
187 rawCosineEvaluatorAtScale q x b * rawBucketAmplitude E b) /
188 q ^ (2 : ℕ)
189 =
190 ((∑ b ∈ rawCosineSupport,
191 rawCosineEvaluatorAtScale q x b * rawBucketAmplitude E b) -
192 ∑ b ∈ rawCosineSupport, rawBucketAmplitude E b) /
193 q ^ (2 : ℕ) := by rw [hzero', sub_zero]
194 _ = ∑ b ∈ rawCosineSupport,
195 ((Real.cos (q * rawPhaseLinear x b) - 1) / q ^ (2 : ℕ)) *
196 rawBucketAmplitude E b := by
197 rw [← Finset.sum_sub_distrib]
198 simp_rw [Finset.sum_div]
199 refine Finset.sum_congr rfl fun b _ => ?_
200 unfold rawCosineEvaluatorAtScale
201 field_simp [hq]
202 refine hsum.congr' hcongr.symm |>.congr' ?_
203 filter_upwards with _
204 rfl
205
206/-- Normalizing the direction divides its phase quadratic by its squared
207norm. -/
208theorem rawPhaseQuadratic_normalized (x : Fin 3 → ℝ)
209 (hx : 0 < realModeNormSq x) (b : Bucket) :
210 rawPhaseQuadratic
211 (fun i => x i / Real.sqrt (realModeNormSq x)) b =
212 rawPhaseQuadratic x b / realModeNormSq x := by
213 have hsqrt : Real.sqrt (realModeNormSq x) ≠ 0 :=
214 ne_of_gt (Real.sqrt_pos.2 hx)
215 have hsqrt_sq :
216 Real.sqrt (realModeNormSq x) ^ (2 : ℕ) = realModeNormSq x :=
217 Real.sq_sqrt hx.le
218 unfold rawPhaseQuadratic rawPhaseLinear
219 simp only [Fin.sum_univ_three]
220 field_simp [hsqrt, hx.ne']
221 nlinarith
222
223/-- `reggeTTMoment` is homogeneous under direction normalization with the
224expected inverse squared-norm factor. -/
225theorem reggeTTMoment_normalized (x : Fin 3 → ℝ)
226 (hx : 0 < realModeNormSq x) (E : Fin 3 → Fin 3 → ℝ) :
227 reggeTTMoment rawCosineSupport
228 (rawPhaseQuadratic
229 (fun i => x i / Real.sqrt (realModeNormSq x)))
230 (rawBucketAmplitude E) =
231 reggeTTMoment rawCosineSupport (rawPhaseQuadratic x)
232 (rawBucketAmplitude E) / realModeNormSq x := by
233 unfold reggeTTMoment reggeTTBlochFold
234 rw [Finset.sum_div]
235 refine Finset.sum_congr rfl fun b _ => ?_
236 show
237 -rawPhaseQuadratic (fun i => x i / Real.sqrt (realModeNormSq x)) b / 2 *
238 rawBucketAmplitude E b =
239 -rawPhaseQuadratic x b / 2 * rawBucketAmplitude E b / realModeNormSq x
240 rw [rawPhaseQuadratic_normalized x hx b]
241 field_simp [hx.ne']
242
243/-- A nonzero integer mode has positive real squared norm. -/
244theorem realModeNormSq_intCast_pos (m : Fin 3 → ℤ)
245 (hm : ∃ i : Fin 3, m i ≠ 0) :
246 0 < realModeNormSq (fun i => (m i : ℝ)) := by
247 obtain ⟨i, hi⟩ := hm
248 unfold realModeNormSq
249 have hi' : (m i : ℝ) ≠ 0 := by exact_mod_cast hi
250 exact Finset.sum_pos' (fun j _ => sq_nonneg (m j : ℝ))
251 ⟨i, Finset.mem_univ i, sq_pos_of_ne_zero hi'⟩
252
253/-- The commensurate evaluator is exactly the free-scale evaluator at
254`q_N = 2*pi/N`. -/
255theorem rawCosineEvaluator_eq_scale (N : ℕ) [NeZero N]
256 (m : Fin 3 → ℤ) (b : Bucket) :
257 rawCosineEvaluator N m b =
258 rawCosineEvaluatorAtScale (sideScale N) (fun i => (m i : ℝ)) b := by
259 unfold rawCosineEvaluator rawCosineEvaluatorAtScale rawPhaseLinear
260 commensurateMomentum sideScale
261 congr 1
262 simp only [Fin.sum_univ_three]
263 ring
264
265/-- Exact factorization of the momentum normalization into scale squared
266times the integer-mode norm squared. -/
267theorem momentumNormSq_eq_scale_sq (N : ℕ) [NeZero N]
268 (m : Fin 3 → ℤ) :
269 momentumNormSq N m =
270 sideScale N ^ (2 : ℕ) * realModeNormSq (fun i => (m i : ℝ)) := by
271 unfold momentumNormSq commensurateMomentum sideScale realModeNormSq
272 simp only [Fin.sum_univ_three]
273 ring
274
275/-- FINAL P1.1a HEADLINE: for every fixed nonzero integer mode, the actual
276finite reduced Regge symbol, divided by `momentumNormSq`, converges to exactly
277the raw Regge TT moment at the normalized real mode direction. The literal
278phase remains `(sum_i x_i * (u_i / 2))^2`. -/
279theorem canonicalFiniteH_div_momentumNormSq_tendsto (E : Fin 3 → Fin 3 → ℝ)
280 (m : Fin 3 → ℤ) (hm : ∃ i : Fin 3, m i ≠ 0) :
281 Filter.Tendsto
282 (fun j : ℕ =>
283 @canonicalFiniteH (j + 3) (instNeZeroAddThree j) E m /
284 momentumNormSq (j + 3) m)
285 Filter.atTop
286 (nhds
287 (reggeTTMoment rawCosineSupport
288 (rawPhaseQuadratic (normalizedRealMode m))
289 (rawBucketAmplitude E))) := by
290 let x : Fin 3 → ℝ := fun i => (m i : ℝ)
291 let s : ℝ := realModeNormSq x
292 have hs : 0 < s := realModeNormSq_intCast_pos m hm
293 have hq0 :
294 Filter.Tendsto (fun j : ℕ => sideScale (j + 3))
295 Filter.atTop (nhds 0) := by
296 have h :=
297 (tendsto_const_div_atTop_nhds_zero_nat (2 * Real.pi)).comp
298 (Filter.tendsto_add_atTop_nat 3)
299 exact h.congr fun j => rfl
300 have hqmem :
301 ∀ᶠ j : ℕ in Filter.atTop,
302 sideScale (j + 3) ∈ ({0}ᶜ : Set ℝ) := by
303 filter_upwards with j
304 have hden : ((j + 3 : ℕ) : ℝ) ≠ 0 := by positivity
305 have hnum : (2 * Real.pi : ℝ) ≠ 0 := mul_ne_zero two_ne_zero Real.pi_ne_zero
306 simp only [Set.mem_compl_iff, Set.mem_singleton_iff]
307 exact div_ne_zero hnum hden
308 have hq :
309 Filter.Tendsto (fun j : ℕ => sideScale (j + 3))
310 Filter.atTop (nhdsWithin 0 {(0 : ℝ)}ᶜ) :=
311 tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within _ hq0 hqmem
312 have hscale :=
313 (rawCosineFold_scale_tendsto x E).comp hq
314 have hdiv := hscale.div_const s
315 have hlimit :
316 Filter.Tendsto
317 (fun j : ℕ =>
318 rawCosineFoldAtScale (sideScale (j + 3)) x E /
319 sideScale (j + 3) ^ (2 : ℕ) / s)
320 Filter.atTop
321 (nhds
322 (reggeTTMoment rawCosineSupport
323 (rawPhaseQuadratic (normalizedRealMode m))
324 (rawBucketAmplitude E))) := by
325 rw [show normalizedRealMode m =
326 fun i => x i / Real.sqrt (realModeNormSq x) by
327 funext i
328 rfl]
329 rw [reggeTTMoment_normalized x hs E]
330 simpa [s] using hdiv
331 have hshift : Filter.Tendsto (fun j : ℕ => j + 3)
332 Filter.atTop Filter.atTop := Filter.tendsto_add_atTop_nat 3
333 have hassembly :=
334 hshift.eventually
335 (eventually_canonicalFiniteH_eq_rawCosineBlochFold E m hm)
336 refine hlimit.congr' ?_
337 filter_upwards [hassembly] with j hj
338 specialize hj (instNeZeroAddThree j)
339 rw [hj, momentumNormSq_eq_scale_sq]
340 unfold rawCosineFoldAtScale reggeTTBlochFold
341 rw [div_div]
342 have hsum_eq :
343 (∑ b ∈ rawCosineSupport,
344 rawCosineEvaluatorAtScale (sideScale (j + 3)) x b *
345 rawBucketAmplitude E b) =
346 ∑ b ∈ rawCosineSupport,
347 rawCosineEvaluator (j + 3) m b * rawBucketAmplitude E b := by
348 refine Finset.sum_congr rfl fun b _ => ?_
349 rw [rawCosineEvaluator_eq_scale]
350 rw [hsum_eq]
351
352end
353
354end ReggeTTContinuumLimit
355end Analysis
356end Gravity
357end IndisputableMonolith
358
359#print axioms IndisputableMonolith.Gravity.Analysis.ReggeTTContinuumLimit.rawCosineFoldAtScale_zero
360#print axioms IndisputableMonolith.Gravity.Analysis.ReggeTTContinuumLimit.rawCosineFold_scale_tendsto
361#print axioms IndisputableMonolith.Gravity.Analysis.ReggeTTContinuumLimit.canonicalFiniteH_div_momentumNormSq_tendsto
362