IndisputableMonolith.Gravity.Analysis.EdgeTTDecompositionLorentz4D
IndisputableMonolith/Gravity/Analysis/EdgeTTDecompositionLorentz4D.lean · 994 lines · 118 declarations
show as:
view math explainer →
1import Mathlib
2import IndisputableMonolith.Gravity.ClausiusEinsteinBridge
3
4/-!
5# Edge TT decomposition (4D), Lorentzian algebraic layer
6
7QG full-theory campaign, Wave 4 / lane W4-1 (`edge_tt_decomposition`),
8Lorentzian specialization of the Euclidean algebraic TT layer in
9`EdgeTTDecomposition4D`: transverse-traceless decomposition of symmetric
10`4 × 4` real matrices against a Minkowski wave covector on `Fin 4`,
11including the physically relevant **null** case.
12
13## Tier tags (binding)
14
15* THEOREM: every named result in this file (kernel-checked; no `sorry`, no
16 `admit`, no new axioms, no `native_decide`, no `: True` shells).
17* This is the Lorentzian linear-algebra layer of the ledger closing name
18 `edge_tt_decomposition`. It does **not** decompose Regge EDGE
19 perturbations on a 4D lattice, does **not** prove `S_RS_converges_EH_4d`,
20 does **not** flip `gap_action_recovery`, and attaches no physical
21 polarization normalization.
22
23## Conventions
24
25Signature `(-,+,+,+)`. Covectors are lowered by default. Index raising
26negates the time component: `(raise v) 0 = -v 0` and `(raise v) i = v i`
27for spatial `i`. The Minkowski pairing of covectors is
28`minkowskiDot a b = -(a 0)(b 0) + (a 1)(b 1) + (a 2)(b 2) + (a 3)(b 3)`,
29equal to `∑ j, a j * (raise b) j`. The metric-trace of a covariant
30symmetric matrix is
31`minkowskiTrace H = -(H 0 0) + H 1 1 + H 2 2 + H 3 3` (`η^{ij} H_{ij}`).
32
33Lorentz transversality contracts the second index of `H` against the
34**raised** wave covector:
35`∀ i, -(H i 0) * m 0 + H i 1 * m 1 + H i 2 * m 2 + H i 3 * m 3 = 0`.
36
37* Non-null: `minkowskiDot m m ≠ 0`, projector
38 `P_{ij} = η_{ij} - m_i m_j / (m·m)`.
39* Null: `minkowskiDot m m = 0`, `m ≠ 0`, with auxiliary null `l` satisfying
40 `minkowskiDot m l ≠ 0`; projector
41 `P_{ij} = η_{ij} - (m_i l_j + l_i m_j) / (m·l)`.
42
43Expected axiom footprint: `[propext, Classical.choice, Quot.sound]`.
44-/
45
46namespace IndisputableMonolith
47namespace Gravity
48namespace Analysis
49namespace EdgeTTDecompositionLorentz4D
50
51open Matrix BigOperators
52open IndisputableMonolith.Gravity.ClausiusEinsteinBridge
53 (minkowskiEta4 MinkowskiNull vec4)
54
55noncomputable section
56
57abbrev Mat4 := Matrix (Fin 4) (Fin 4) ℝ
58
59def IsSymmetric (H : Mat4) : Prop :=
60 ∀ i j : Fin 4, H i j = H j i
61
62/-- Index raising for the `(-,+,+,+)` metric: negate the time component. -/
63def raise (v : Fin 4 → ℝ) : Fin 4 → ℝ :=
64 fun i => if i = 0 then -v 0 else v i
65
66/-- Minkowski pairing of covectors: `η^{ij} a_i b_j`. -/
67def minkowskiDot (a b : Fin 4 → ℝ) : ℝ :=
68 -(a 0) * (b 0) + (a 1) * (b 1) + (a 2) * (b 2) + (a 3) * (b 3)
69
70/-- Metric trace of a covariant matrix: `η^{ij} H_{ij}`. -/
71def minkowskiTrace (H : Mat4) : ℝ :=
72 -(H 0 0) + H 1 1 + H 2 2 + H 3 3
73
74def IsLorentzTraceless (H : Mat4) : Prop :=
75 minkowskiTrace H = 0
76
77/-- Lorentz transversality: contract `H_{ij}` with raised `m^j`. -/
78def IsLorentzTransverse (m : Fin 4 → ℝ) (H : Mat4) : Prop :=
79 ∀ i : Fin 4, -(H i 0) * m 0 + H i 1 * m 1 + H i 2 * m 2 + H i 3 * m 3 = 0
80
81/-- Algebraic Lorentz TT: symmetric, Minkowski-traceless, Lorentz-transverse. -/
82def IsLorentzTT (m : Fin 4 → ℝ) (H : Mat4) : Prop :=
83 IsSymmetric H ∧ IsLorentzTraceless H ∧ IsLorentzTransverse m H
84
85def minkowskiEta : Mat4 := minkowskiEta4
86
87def gaugePart (m v : Fin 4 → ℝ) : Mat4 :=
88 fun i j => m i * v j + v i * m j
89
90def outerSq (m : Fin 4 → ℝ) : Mat4 :=
91 fun i j => m i * m j
92
93def symmetrizedOuter (m l : Fin 4 → ℝ) : Mat4 :=
94 fun i j => m i * l j + l i * m j
95
96/-- Lorentz load: `(H · m^♯)_i`. -/
97def lorentzLoad (H : Mat4) (m : Fin 4 → ℝ) : Fin 4 → ℝ :=
98 fun i => ∑ j : Fin 4, H i j * raise m j
99
100theorem lorentzLoad_eq (H : Mat4) (m : Fin 4 → ℝ) (i : Fin 4) :
101 lorentzLoad H m i =
102 -(H i 0) * m 0 + H i 1 * m 1 + H i 2 * m 2 + H i 3 * m 3 := by
103 unfold lorentzLoad raise
104 simp [Fin.sum_univ_four]
105
106theorem IsLorentzTransverse_iff_lorentzLoad (m : Fin 4 → ℝ) (H : Mat4) :
107 IsLorentzTransverse m H ↔ ∀ i, lorentzLoad H m i = 0 := by
108 constructor
109 · intro h i; rw [lorentzLoad_eq]; exact h i
110 · intro h i; rw [← lorentzLoad_eq]; exact h i
111
112theorem minkowskiDot_eq_sum (a b : Fin 4 → ℝ) :
113 minkowskiDot a b = ∑ i : Fin 4, a i * raise b i := by
114 unfold minkowskiDot raise
115 simp [Fin.sum_univ_four]
116
117theorem minkowskiDot_comm (a b : Fin 4 → ℝ) :
118 minkowskiDot a b = minkowskiDot b a := by
119 unfold minkowskiDot; ring
120
121theorem minkowskiTrace_eq_sum (H : Mat4) :
122 minkowskiTrace H = ∑ i : Fin 4, ∑ j : Fin 4, minkowskiEta i j * H i j := by
123 unfold minkowskiTrace minkowskiEta minkowskiEta4
124 simp [Fin.sum_univ_four]
125
126/-! ## §1. Elementary identities -/
127
128theorem gaugePart_symmetric (m v : Fin 4 → ℝ) :
129 IsSymmetric (gaugePart m v) := by
130 intro i j; unfold gaugePart; ring
131
132theorem outerSq_symmetric (m : Fin 4 → ℝ) :
133 IsSymmetric (outerSq m) := by
134 intro i j; unfold outerSq; ring
135
136theorem symmetrizedOuter_symmetric (m l : Fin 4 → ℝ) :
137 IsSymmetric (symmetrizedOuter m l) := by
138 intro i j; unfold symmetrizedOuter; ring
139
140theorem raise_raise (v : Fin 4 → ℝ) : raise (raise v) = v := by
141 funext i
142 unfold raise
143 by_cases h : i = 0
144 · subst h; simp
145 · simp [h]
146
147theorem lorentzLoad_smul (c : ℝ) (H : Mat4) (m : Fin 4 → ℝ) (i : Fin 4) :
148 lorentzLoad (c • H) m i = c * lorentzLoad H m i := by
149 unfold lorentzLoad
150 simp only [smul_apply, smul_eq_mul, mul_assoc]
151 exact (Finset.mul_sum Finset.univ (fun j => H i j * raise m j) c).symm
152
153theorem lorentzLoad_sub (A B : Mat4) (m : Fin 4 → ℝ) (i : Fin 4) :
154 lorentzLoad (A - B) m i = lorentzLoad A m i - lorentzLoad B m i := by
155 unfold lorentzLoad; simp [sub_mul, Finset.sum_sub_distrib]
156
157theorem lorentzLoad_eta (m : Fin 4 → ℝ) (i : Fin 4) :
158 lorentzLoad minkowskiEta m i = m i := by
159 rw [lorentzLoad_eq]
160 unfold minkowskiEta minkowskiEta4
161 fin_cases i <;> simp <;> ring_nf
162
163theorem lorentzLoad_outerSq (m : Fin 4 → ℝ) (i : Fin 4) :
164 lorentzLoad (outerSq m) m i = minkowskiDot m m * m i := by
165 unfold lorentzLoad outerSq
166 calc
167 ∑ j : Fin 4, (m i * m j) * raise m j
168 = m i * ∑ j : Fin 4, m j * raise m j := by
169 simp [mul_assoc, Finset.mul_sum]
170 _ = m i * minkowskiDot m m := by rw [← minkowskiDot_eq_sum]
171 _ = minkowskiDot m m * m i := by ring
172
173theorem lorentzLoad_symmetrizedOuter (m l : Fin 4 → ℝ) (i : Fin 4) :
174 lorentzLoad (symmetrizedOuter m l) m i =
175 minkowskiDot l m * m i + minkowskiDot m m * l i := by
176 unfold lorentzLoad symmetrizedOuter
177 calc
178 ∑ j : Fin 4, (m i * l j + l i * m j) * raise m j
179 = ∑ j : Fin 4, (m i * (l j * raise m j) + l i * (m j * raise m j)) := by
180 refine Finset.sum_congr rfl fun j _ => by ring
181 _ = (∑ j : Fin 4, m i * (l j * raise m j)) +
182 (∑ j : Fin 4, l i * (m j * raise m j)) := Finset.sum_add_distrib
183 _ = m i * ∑ j : Fin 4, l j * raise m j +
184 l i * ∑ j : Fin 4, m j * raise m j := by
185 simp [Finset.mul_sum]
186 _ = m i * minkowskiDot l m + l i * minkowskiDot m m := by
187 simp [← minkowskiDot_eq_sum]
188 _ = minkowskiDot l m * m i + minkowskiDot m m * l i := by ring
189
190theorem lorentzLoad_symmetrizedOuter_l (m l : Fin 4 → ℝ) (i : Fin 4) :
191 lorentzLoad (symmetrizedOuter m l) l i =
192 minkowskiDot l l * m i + minkowskiDot m l * l i := by
193 unfold lorentzLoad symmetrizedOuter
194 calc
195 ∑ j : Fin 4, (m i * l j + l i * m j) * raise l j
196 = ∑ j : Fin 4, (m i * (l j * raise l j) + l i * (m j * raise l j)) := by
197 refine Finset.sum_congr rfl fun j _ => by ring
198 _ = (∑ j : Fin 4, m i * (l j * raise l j)) +
199 (∑ j : Fin 4, l i * (m j * raise l j)) := Finset.sum_add_distrib
200 _ = m i * ∑ j : Fin 4, l j * raise l j +
201 l i * ∑ j : Fin 4, m j * raise l j := by
202 simp [Finset.mul_sum]
203 _ = m i * minkowskiDot l l + l i * minkowskiDot m l := by
204 simp [← minkowskiDot_eq_sum]
205 _ = minkowskiDot l l * m i + minkowskiDot m l * l i := by ring
206
207theorem lorentzLoad_gaugePart (m v : Fin 4 → ℝ) (i : Fin 4) :
208 lorentzLoad (gaugePart m v) m i =
209 minkowskiDot m m * v i + m i * minkowskiDot v m := by
210 unfold lorentzLoad gaugePart
211 calc
212 ∑ j : Fin 4, (m i * v j + v i * m j) * raise m j
213 = ∑ j : Fin 4, (m i * (v j * raise m j) + v i * (m j * raise m j)) := by
214 refine Finset.sum_congr rfl fun j _ => by ring
215 _ = (∑ j : Fin 4, m i * (v j * raise m j)) +
216 (∑ j : Fin 4, v i * (m j * raise m j)) := Finset.sum_add_distrib
217 _ = m i * ∑ j : Fin 4, v j * raise m j +
218 v i * ∑ j : Fin 4, m j * raise m j := by
219 simp [Finset.mul_sum]
220 _ = m i * minkowskiDot v m + v i * minkowskiDot m m := by
221 simp [← minkowskiDot_eq_sum]
222 _ = minkowskiDot m m * v i + m i * minkowskiDot v m := by ring
223
224theorem minkowskiTrace_smul (c : ℝ) (H : Mat4) :
225 minkowskiTrace (c • H) = c * minkowskiTrace H := by
226 unfold minkowskiTrace
227 simp only [smul_apply, smul_eq_mul]
228 ring
229
230theorem minkowskiTrace_sub (A B : Mat4) :
231 minkowskiTrace (A - B) = minkowskiTrace A - minkowskiTrace B := by
232 unfold minkowskiTrace
233 simp only [sub_apply]
234 ring
235
236theorem minkowskiTrace_add (A B : Mat4) :
237 minkowskiTrace (A + B) = minkowskiTrace A + minkowskiTrace B := by
238 unfold minkowskiTrace
239 simp only [add_apply]
240 ring
241
242theorem minkowskiTrace_eta : minkowskiTrace minkowskiEta = 4 := by
243 unfold minkowskiTrace minkowskiEta minkowskiEta4
244 simp; norm_num
245
246theorem minkowskiTrace_outerSq (m : Fin 4 → ℝ) :
247 minkowskiTrace (outerSq m) = minkowskiDot m m := by
248 unfold minkowskiTrace outerSq minkowskiDot; ring
249
250theorem minkowskiTrace_symmetrizedOuter (m l : Fin 4 → ℝ) :
251 minkowskiTrace (symmetrizedOuter m l) = 2 * minkowskiDot m l := by
252 unfold minkowskiTrace symmetrizedOuter minkowskiDot; ring
253
254theorem minkowskiDot_eq_MinkowskiNull (k : Fin 4 → ℝ) :
255 minkowskiDot k k = 0 ↔ MinkowskiNull k := by
256 unfold minkowskiDot MinkowskiNull
257 constructor <;> intro h <;> linarith
258
259/-! ## §2. Non-null transverse projector and gauge removal -/
260
261def transverseProjector (m : Fin 4 → ℝ) : Mat4 :=
262 minkowskiEta - (minkowskiDot m m)⁻¹ • outerSq m
263
264def gaugeVector (m : Fin 4 → ℝ) (H : Mat4) : Fin 4 → ℝ :=
265 fun i =>
266 let w := lorentzLoad H m
267 let s := minkowskiDot m m
268 w i / s - m i * minkowskiDot w m / (2 * s ^ 2)
269
270def gaugeCorrected (m : Fin 4 → ℝ) (H : Mat4) : Mat4 :=
271 H - gaugePart m (gaugeVector m H)
272
273def residualTrace (m : Fin 4 → ℝ) (H : Mat4) : ℝ :=
274 minkowskiTrace (gaugeCorrected m H) / 3
275
276def ttProject (m : Fin 4 → ℝ) (H : Mat4) : Mat4 :=
277 gaugeCorrected m H - residualTrace m H • transverseProjector m
278
279theorem minkowskiEta_symmetric : IsSymmetric minkowskiEta := by
280 intro i j
281 unfold minkowskiEta minkowskiEta4
282 by_cases hij : i = j
283 · subst hij; rfl
284 · simp [hij, Ne.symm hij]
285
286theorem transverseProjector_symmetric (m : Fin 4 → ℝ) :
287 IsSymmetric (transverseProjector m) := by
288 intro i j
289 unfold transverseProjector
290 simp only [sub_apply, smul_apply, smul_eq_mul]
291 rw [minkowskiEta_symmetric i j, outerSq_symmetric m i j]
292
293theorem lorentzLoad_transverseProjector (m : Fin 4 → ℝ)
294 (hm : minkowskiDot m m ≠ 0) (i : Fin 4) :
295 lorentzLoad (transverseProjector m) m i = 0 := by
296 unfold transverseProjector
297 rw [lorentzLoad_sub, lorentzLoad_eta, lorentzLoad_smul, lorentzLoad_outerSq]
298 field_simp [hm]; ring
299
300theorem minkowskiDot_gaugeVector (m : Fin 4 → ℝ) (H : Mat4)
301 (hm : minkowskiDot m m ≠ 0) :
302 minkowskiDot (gaugeVector m H) m =
303 minkowskiDot (lorentzLoad H m) m / (2 * minkowskiDot m m) := by
304 set w := lorentzLoad H m with hw
305 set s := minkowskiDot m m with hs
306 have hs0 : s ≠ 0 := hm
307 set d := minkowskiDot w m with hd
308 have hexpand :
309 minkowskiDot (gaugeVector m H) m =
310 ∑ i : Fin 4, (w i / s - m i * d / (2 * s ^ 2)) * raise m i := by
311 simp only [minkowskiDot_eq_sum, gaugeVector, w, s, d]
312 have hsplit :
313 ∑ i : Fin 4, (w i / s - m i * d / (2 * s ^ 2)) * raise m i =
314 ∑ i : Fin 4, (w i / s) * raise m i -
315 ∑ i : Fin 4, (m i * d / (2 * s ^ 2)) * raise m i := by
316 simp [sub_mul, Finset.sum_sub_distrib]
317 have h1 : ∑ i : Fin 4, (w i / s) * raise m i = d / s := by
318 simp only [d, minkowskiDot_eq_sum, div_eq_mul_inv, mul_assoc]
319 have :
320 ∑ i : Fin 4, s⁻¹ * w i * raise m i =
321 s⁻¹ * ∑ i : Fin 4, w i * raise m i := by
322 simp [mul_assoc, ← Finset.mul_sum]
323 convert this using 1
324 · refine Finset.sum_congr rfl fun i _ => by ring
325 · ring
326 have h2 :
327 ∑ i : Fin 4, (m i * d / (2 * s ^ 2)) * raise m i =
328 s * d / (2 * s ^ 2) := by
329 have :
330 ∑ i : Fin 4, m i * raise m i * (d / (2 * s ^ 2)) =
331 (∑ i : Fin 4, m i * raise m i) * (d / (2 * s ^ 2)) :=
332 (Finset.sum_mul _ _ _).symm
333 calc
334 ∑ i : Fin 4, (m i * d / (2 * s ^ 2)) * raise m i
335 = ∑ i : Fin 4, m i * raise m i * (d / (2 * s ^ 2)) := by
336 refine Finset.sum_congr rfl fun i _ => by ring
337 _ = (∑ i : Fin 4, m i * raise m i) * (d / (2 * s ^ 2)) := this
338 _ = s * d / (2 * s ^ 2) := by
339 simp [← minkowskiDot_eq_sum, s]; ring
340 calc
341 minkowskiDot (gaugeVector m H) m
342 = ∑ i : Fin 4, (w i / s - m i * d / (2 * s ^ 2)) * raise m i := hexpand
343 _ = d / s - s * d / (2 * s ^ 2) := by rw [hsplit, h1, h2]
344 _ = d / (2 * s) := by field_simp [hs0]; ring
345 _ = minkowskiDot (lorentzLoad H m) m / (2 * minkowskiDot m m) := by
346 simp [d, w, s]
347
348theorem lorentzLoad_gaugePart_gaugeVector (m : Fin 4 → ℝ) (H : Mat4)
349 (hm : minkowskiDot m m ≠ 0) (i : Fin 4) :
350 lorentzLoad (gaugePart m (gaugeVector m H)) m i = lorentzLoad H m i := by
351 set w := lorentzLoad H m
352 set s := minkowskiDot m m
353 set v := gaugeVector m H
354 have hs0 : s ≠ 0 := hm
355 have hL := lorentzLoad_gaugePart m v i
356 have hdot := minkowskiDot_gaugeVector m H hm
357 have hvi : v i = w i / s - m i * minkowskiDot w m / (2 * s ^ 2) := rfl
358 have key : s * v i + m i * minkowskiDot v m = w i := by
359 rw [hvi, show minkowskiDot v m = minkowskiDot w m / (2 * s) from hdot]
360 field_simp [hs0]; ring
361 rw [hL]; simpa [s, w, v] using key
362
363theorem gaugeCorrected_transverse (m : Fin 4 → ℝ) (H : Mat4)
364 (hm : minkowskiDot m m ≠ 0) :
365 IsLorentzTransverse m (gaugeCorrected m H) := by
366 intro i
367 rw [← lorentzLoad_eq]
368 simp [gaugeCorrected, lorentzLoad_sub, lorentzLoad_gaugePart_gaugeVector m H hm]
369
370theorem gaugeCorrected_symmetric (m : Fin 4 → ℝ) (H : Mat4)
371 (hH : IsSymmetric H) :
372 IsSymmetric (gaugeCorrected m H) := by
373 intro i j
374 simp only [gaugeCorrected, sub_apply]
375 rw [hH i j, gaugePart_symmetric m (gaugeVector m H) i j]
376
377theorem minkowskiTrace_transverseProjector (m : Fin 4 → ℝ)
378 (hm : minkowskiDot m m ≠ 0) :
379 minkowskiTrace (transverseProjector m) = 3 := by
380 unfold transverseProjector
381 rw [minkowskiTrace_sub, minkowskiTrace_smul, minkowskiTrace_eta,
382 minkowskiTrace_outerSq]
383 field_simp [hm]; ring
384
385theorem ttProject_symmetric (m : Fin 4 → ℝ) (H : Mat4)
386 (hH : IsSymmetric H) :
387 IsSymmetric (ttProject m H) := by
388 intro i j
389 simp only [ttProject, sub_apply, smul_apply, smul_eq_mul]
390 rw [gaugeCorrected_symmetric m H hH i j,
391 transverseProjector_symmetric m i j]
392
393theorem ttProject_transverse (m : Fin 4 → ℝ) (H : Mat4)
394 (hm : minkowskiDot m m ≠ 0) :
395 IsLorentzTransverse m (ttProject m H) := by
396 intro i
397 rw [← lorentzLoad_eq]
398 have h1 : lorentzLoad (gaugeCorrected m H) m i = 0 := by
399 rw [lorentzLoad_eq]; exact gaugeCorrected_transverse m H hm i
400 have h2 := lorentzLoad_transverseProjector m hm i
401 simp [ttProject, lorentzLoad_sub, lorentzLoad_smul, h1, h2]
402
403theorem ttProject_traceless (m : Fin 4 → ℝ) (H : Mat4)
404 (hm : minkowskiDot m m ≠ 0) :
405 IsLorentzTraceless (ttProject m H) := by
406 unfold IsLorentzTraceless ttProject residualTrace
407 rw [minkowskiTrace_sub, minkowskiTrace_smul,
408 minkowskiTrace_transverseProjector m hm]
409 ring
410
411theorem ttProject_isLorentzTT (m : Fin 4 → ℝ) (H : Mat4)
412 (hH : IsSymmetric H) (hm : minkowskiDot m m ≠ 0) :
413 IsLorentzTT m (ttProject m H) :=
414 ⟨ttProject_symmetric m H hH, ttProject_traceless m H hm,
415 ttProject_transverse m H hm⟩
416
417/-- **THEOREM (non-null Lorentzian algebraic `edge_tt_decomposition`).**
418Every symmetric `4 × 4` matrix against a non-null Minkowski wave covector
419decomposes as Lorentz-TT + gauge + transverse-trace part. -/
420theorem exists_lorentzTTDecomposition (m : Fin 4 → ℝ) (H : Mat4)
421 (hH : IsSymmetric H) (hm : minkowskiDot m m ≠ 0) :
422 H = ttProject m H + gaugePart m (gaugeVector m H) +
423 residualTrace m H • transverseProjector m ∧
424 IsLorentzTT m (ttProject m H) := by
425 refine ⟨?_, ttProject_isLorentzTT m H hH hm⟩
426 unfold ttProject gaugeCorrected; abel
427
428theorem exists_lorentzTTDecomposition' (m : Fin 4 → ℝ) (H : Mat4)
429 (hH : IsSymmetric H) (hm : minkowskiDot m m ≠ 0) :
430 ∃ (H_TT : Mat4) (v : Fin 4 → ℝ) (β : ℝ),
431 H = H_TT + gaugePart m v + β • transverseProjector m ∧
432 IsLorentzTT m H_TT :=
433 ⟨ttProject m H, gaugeVector m H, residualTrace m H,
434 exists_lorentzTTDecomposition m H hH hm⟩
435
436/-! ## §3. Null-frame projector -/
437
438/-- Null-frame transverse projector against null `m` with auxiliary null `l`. -/
439def nullProjector (m l : Fin 4 → ℝ) : Mat4 :=
440 minkowskiEta - (minkowskiDot m l)⁻¹ • symmetrizedOuter m l
441
442def nullSMixed (m l : Fin 4 → ℝ) (i a : Fin 4) : ℝ :=
443 (m i * raise l a + l i * raise m a) / minkowskiDot m l
444
445def kron (i j : Fin 4) : ℝ := if i = j then 1 else 0
446
447def nullPMixed (m l : Fin 4 → ℝ) (i a : Fin 4) : ℝ :=
448 kron i a - nullSMixed m l i a
449
450/-- Double mixed projection `(P H P)_{ij} = P_i{}^a H_{ab} P_j{}^b`. -/
451def nullPhp (m l : Fin 4 → ℝ) (H : Mat4) : Mat4 :=
452 fun i j => ∑ a : Fin 4, ∑ b : Fin 4,
453 nullPMixed m l i a * H a b * nullPMixed m l j b
454
455/-- Bilinear remainder `S H S` in the null gap expansion. -/
456def nullBilinear (m l : Fin 4 → ℝ) (H : Mat4) : Mat4 :=
457 fun i j => ∑ a : Fin 4, ∑ b : Fin 4,
458 nullSMixed m l i a * H a b * nullSMixed m l j b
459
460def nullMGaugeVector (m l : Fin 4 → ℝ) (H : Mat4) : Fin 4 → ℝ :=
461 fun j => lorentzLoad H l j / minkowskiDot m l
462
463def nullLGaugeVector (m l : Fin 4 → ℝ) (H : Mat4) : Fin 4 → ℝ :=
464 fun j => lorentzLoad H m j / minkowskiDot m l
465
466/-- Explicit gap `H - PHP = gauge_m + gauge_l - SHS`. -/
467def nullGap (m l : Fin 4 → ℝ) (H : Mat4) : Mat4 :=
468 gaugePart m (nullMGaugeVector m l H) +
469 gaugePart l (nullLGaugeVector m l H) -
470 nullBilinear m l H
471
472def nullTraceCoeff (m l : Fin 4 → ℝ) (H : Mat4) : ℝ :=
473 minkowskiTrace (nullPhp m l H) / 2
474
475def nullTTProject (m l : Fin 4 → ℝ) (H : Mat4) : Mat4 :=
476 nullPhp m l H - nullTraceCoeff m l H • nullProjector m l
477
478theorem nullProjector_symmetric (m l : Fin 4 → ℝ) :
479 IsSymmetric (nullProjector m l) := by
480 intro i j
481 unfold nullProjector
482 simp only [sub_apply, smul_apply, smul_eq_mul]
483 rw [minkowskiEta_symmetric i j, symmetrizedOuter_symmetric m l i j]
484
485theorem nullProjector_minkowskiTrace (m l : Fin 4 → ℝ)
486 (hml : minkowskiDot m l ≠ 0) :
487 minkowskiTrace (nullProjector m l) = 2 := by
488 unfold nullProjector
489 rw [minkowskiTrace_sub, minkowskiTrace_smul, minkowskiTrace_eta,
490 minkowskiTrace_symmetrizedOuter]
491 field_simp [hml]; ring
492
493theorem lorentzLoad_nullProjector_m (m l : Fin 4 → ℝ)
494 (hm0 : minkowskiDot m m = 0) (hml : minkowskiDot m l ≠ 0)
495 (i : Fin 4) :
496 lorentzLoad (nullProjector m l) m i = 0 := by
497 unfold nullProjector
498 rw [lorentzLoad_sub, lorentzLoad_eta, lorentzLoad_smul,
499 lorentzLoad_symmetrizedOuter, minkowskiDot_comm l m, hm0]
500 field_simp [hml]; ring
501
502theorem lorentzLoad_nullProjector_l (m l : Fin 4 → ℝ)
503 (hl0 : minkowskiDot l l = 0) (hml : minkowskiDot m l ≠ 0)
504 (i : Fin 4) :
505 lorentzLoad (nullProjector m l) l i = 0 := by
506 unfold nullProjector
507 rw [lorentzLoad_sub, lorentzLoad_eta, lorentzLoad_smul,
508 lorentzLoad_symmetrizedOuter_l, hl0]
509 field_simp [hml]; ring
510
511theorem sum_kron_left (i : Fin 4) (f : Fin 4 → ℝ) :
512 (∑ a : Fin 4, kron i a * f a) = f i := by
513 unfold kron
514 rw [Finset.sum_eq_single (a := i)]
515 · simp
516 · intro a _ ha
517 rw [if_neg (Ne.symm ha)]; simp
518 · intro hi; exact (hi (Finset.mem_univ i)).elim
519
520theorem sum_kron_right (j : Fin 4) (f : Fin 4 → ℝ) :
521 (∑ b : Fin 4, f b * kron j b) = f j := by
522 unfold kron
523 rw [Finset.sum_eq_single (a := j)]
524 · simp
525 · intro b _ hb
526 rw [if_neg (Ne.symm hb)]; simp
527 · intro hj; exact (hj (Finset.mem_univ j)).elim
528
529theorem nullPhp_expand_algebra (m l : Fin 4 → ℝ) (H : Mat4) (i j : Fin 4) :
530 (∑ a : Fin 4, ∑ b : Fin 4,
531 (kron i a - nullSMixed m l i a) * H a b *
532 (kron j b - nullSMixed m l j b)) =
533 (∑ a : Fin 4, ∑ b : Fin 4, kron i a * H a b * kron j b)
534 - (∑ a : Fin 4, ∑ b : Fin 4, nullSMixed m l i a * H a b * kron j b)
535 - (∑ a : Fin 4, ∑ b : Fin 4, kron i a * H a b * nullSMixed m l j b)
536 + (∑ a : Fin 4, ∑ b : Fin 4,
537 nullSMixed m l i a * H a b * nullSMixed m l j b) := by
538 have hpoint (a b : Fin 4) :
539 (kron i a - nullSMixed m l i a) * H a b *
540 (kron j b - nullSMixed m l j b) =
541 kron i a * H a b * kron j b
542 - nullSMixed m l i a * H a b * kron j b
543 - kron i a * H a b * nullSMixed m l j b
544 + nullSMixed m l i a * H a b * nullSMixed m l j b := by
545 ring
546 simp_rw [hpoint]
547 simp [Finset.sum_sub_distrib, Finset.sum_add_distrib]
548
549theorem sum_kron_H_kron (H : Mat4) (i j : Fin 4) :
550 (∑ a : Fin 4, ∑ b : Fin 4, kron i a * H a b * kron j b) = H i j := by
551 calc
552 ∑ a : Fin 4, ∑ b : Fin 4, kron i a * H a b * kron j b
553 = ∑ a : Fin 4, kron i a * (∑ b : Fin 4, H a b * kron j b) := by
554 refine Finset.sum_congr rfl fun a _ => ?_
555 simp [mul_assoc, Finset.mul_sum]
556 _ = ∑ a : Fin 4, kron i a * H a j := by
557 refine Finset.sum_congr rfl fun a _ => ?_
558 rw [sum_kron_right]
559 _ = H i j := sum_kron_left i _
560
561theorem sum_S_H_kron (m l : Fin 4 → ℝ) (H : Mat4) (i j : Fin 4) :
562 (∑ a : Fin 4, ∑ b : Fin 4, nullSMixed m l i a * H a b * kron j b) =
563 ∑ a : Fin 4, nullSMixed m l i a * H a j := by
564 refine Finset.sum_congr rfl fun a _ => ?_
565 have :
566 (∑ b : Fin 4, nullSMixed m l i a * H a b * kron j b) =
567 nullSMixed m l i a * ∑ b : Fin 4, H a b * kron j b := by
568 simp [mul_assoc, Finset.mul_sum]
569 rw [this, sum_kron_right]
570
571theorem sum_kron_H_S (m l : Fin 4 → ℝ) (H : Mat4) (i j : Fin 4) :
572 (∑ a : Fin 4, ∑ b : Fin 4, kron i a * H a b * nullSMixed m l j b) =
573 ∑ b : Fin 4, H i b * nullSMixed m l j b := by
574 calc
575 ∑ a : Fin 4, ∑ b : Fin 4, kron i a * H a b * nullSMixed m l j b
576 = ∑ a : Fin 4, kron i a * ∑ b : Fin 4, H a b * nullSMixed m l j b := by
577 refine Finset.sum_congr rfl fun a _ => ?_
578 simp [mul_assoc, Finset.mul_sum]
579 _ = ∑ b : Fin 4, H i b * nullSMixed m l j b := by
580 rw [sum_kron_left]
581
582theorem nullPhp_entry (m l : Fin 4 → ℝ) (H : Mat4) (i j : Fin 4) :
583 nullPhp m l H i j =
584 H i j
585 - (∑ a : Fin 4, nullSMixed m l i a * H a j)
586 - (∑ b : Fin 4, H i b * nullSMixed m l j b)
587 + nullBilinear m l H i j := by
588 have hexpand := nullPhp_expand_algebra m l H i j
589 simp only [nullPhp, nullPMixed, nullBilinear]
590 rw [hexpand, sum_kron_H_kron, sum_S_H_kron, sum_kron_H_S]
591
592theorem sum_nullSMixed_H_col (m l : Fin 4 → ℝ) (H : Mat4)
593 (hH : IsSymmetric H) (hml : minkowskiDot m l ≠ 0) (i j : Fin 4) :
594 (∑ a : Fin 4, nullSMixed m l i a * H a j) =
595 m i * (lorentzLoad H l j / minkowskiDot m l) +
596 l i * (lorentzLoad H m j / minkowskiDot m l) := by
597 set s := minkowskiDot m l with hs
598 have hs0 : s ≠ 0 := hml
599 have hterm (a : Fin 4) :
600 nullSMixed m l i a * H a j =
601 (m i / s) * (raise l a * H a j) + (l i / s) * (raise m a * H a j) := by
602 unfold nullSMixed
603 field_simp [hs0, s]; ring
604 have hcol (v : Fin 4 → ℝ) :
605 (∑ a : Fin 4, raise v a * H a j) = lorentzLoad H v j := by
606 unfold lorentzLoad
607 refine Finset.sum_congr rfl fun a _ => ?_
608 rw [hH a j, mul_comm]
609 simp_rw [hterm, Finset.sum_add_distrib, ← Finset.mul_sum, hcol]
610 field_simp [hs0]
611
612theorem sum_H_nullSMixed_row (m l : Fin 4 → ℝ) (H : Mat4)
613 (hml : minkowskiDot m l ≠ 0) (i j : Fin 4) :
614 (∑ b : Fin 4, H i b * nullSMixed m l j b) =
615 m j * (lorentzLoad H l i / minkowskiDot m l) +
616 l j * (lorentzLoad H m i / minkowskiDot m l) := by
617 set s := minkowskiDot m l with hs
618 have hs0 : s ≠ 0 := hml
619 have hterm (b : Fin 4) :
620 H i b * nullSMixed m l j b =
621 (m j / s) * (H i b * raise l b) + (l j / s) * (H i b * raise m b) := by
622 unfold nullSMixed
623 field_simp [hs0, s]; ring
624 simp_rw [hterm, Finset.sum_add_distrib, ← Finset.mul_sum]
625 simp only [lorentzLoad]
626 field_simp [hs0]
627
628theorem nullGap_entry (m l : Fin 4 → ℝ) (H : Mat4)
629 (hH : IsSymmetric H) (hml : minkowskiDot m l ≠ 0) (i j : Fin 4) :
630 nullGap m l H i j =
631 (∑ a : Fin 4, nullSMixed m l i a * H a j) +
632 (∑ b : Fin 4, H i b * nullSMixed m l j b) -
633 nullBilinear m l H i j := by
634 unfold nullGap gaugePart nullMGaugeVector nullLGaugeVector
635 simp only [add_apply, sub_apply]
636 rw [sum_nullSMixed_H_col m l H hH hml i j,
637 sum_H_nullSMixed_row m l H hml i j]
638 ring
639
640/-- Explicit residual identity: `H = PHP + m-gauge + l-gauge - bilinear`. -/
641theorem null_gap_expansion (m l : Fin 4 → ℝ) (H : Mat4)
642 (hH : IsSymmetric H) (hml : minkowskiDot m l ≠ 0) :
643 H = nullPhp m l H + nullGap m l H := by
644 ext i j
645 have hphp := nullPhp_entry m l H i j
646 have hgap := nullGap_entry m l H hH hml i j
647 simp only [add_apply]
648 linarith
649
650theorem nullPhp_symmetric (m l : Fin 4 → ℝ) (H : Mat4)
651 (hH : IsSymmetric H) :
652 IsSymmetric (nullPhp m l H) := by
653 intro i j
654 unfold nullPhp
655 calc
656 ∑ a : Fin 4, ∑ b : Fin 4,
657 nullPMixed m l i a * H a b * nullPMixed m l j b
658 = ∑ b : Fin 4, ∑ a : Fin 4,
659 nullPMixed m l i a * H a b * nullPMixed m l j b := by
660 rw [Finset.sum_comm]
661 _ = ∑ b : Fin 4, ∑ a : Fin 4,
662 nullPMixed m l j b * H b a * nullPMixed m l i a := by
663 refine Finset.sum_congr rfl fun b _ => Finset.sum_congr rfl fun a _ => ?_
664 rw [hH a b]; ring
665 _ = ∑ a : Fin 4, ∑ b : Fin 4,
666 nullPMixed m l j a * H a b * nullPMixed m l i b := by
667 rw [Finset.sum_comm]
668
669/-- Core: `∑ j, S j b * m^j = m^b` when `m` is null. -/
670theorem sum_nullSMixed_raise_m (m l : Fin 4 → ℝ)
671 (hm0 : minkowskiDot m m = 0) (hml : minkowskiDot m l ≠ 0)
672 (b : Fin 4) :
673 (∑ j : Fin 4, nullSMixed m l j b * raise m j) = raise m b := by
674 set s := minkowskiDot m l with hs
675 have hs0 : s ≠ 0 := hml
676 have hterm (j : Fin 4) :
677 nullSMixed m l j b * raise m j =
678 (raise l b / s) * (m j * raise m j) +
679 (raise m b / s) * (l j * raise m j) := by
680 unfold nullSMixed
681 field_simp [hs0, s]; ring
682 simp_rw [hterm, Finset.sum_add_distrib, ← Finset.mul_sum]
683 simp only [← minkowskiDot_eq_sum]
684 rw [hm0, minkowskiDot_comm l m]
685 field_simp [hs0]; ring
686
687theorem sum_nullPMixed_raise_m (m l : Fin 4 → ℝ)
688 (hm0 : minkowskiDot m m = 0) (hml : minkowskiDot m l ≠ 0)
689 (b : Fin 4) :
690 (∑ j : Fin 4, nullPMixed m l j b * raise m j) = 0 := by
691 unfold nullPMixed
692 simp only [sub_mul, Finset.sum_sub_distrib]
693 have hδ : (∑ j : Fin 4, kron j b * raise m j) = raise m b := by
694 -- kron j b = kron b j
695 have : ∀ j, kron j b = kron b j := by
696 intro j; unfold kron; simp [eq_comm]
697 simp_rw [this]
698 exact sum_kron_left b (raise m)
699 rw [hδ, sum_nullSMixed_raise_m m l hm0 hml b]
700 ring
701
702theorem sum_nullSMixed_raise_l (m l : Fin 4 → ℝ)
703 (hl0 : minkowskiDot l l = 0) (hml : minkowskiDot m l ≠ 0)
704 (b : Fin 4) :
705 (∑ j : Fin 4, nullSMixed m l j b * raise l j) = raise l b := by
706 set s := minkowskiDot m l with hs
707 have hs0 : s ≠ 0 := hml
708 have hterm (j : Fin 4) :
709 nullSMixed m l j b * raise l j =
710 (raise l b / s) * (m j * raise l j) +
711 (raise m b / s) * (l j * raise l j) := by
712 unfold nullSMixed
713 field_simp [hs0, s]; ring
714 simp_rw [hterm, Finset.sum_add_distrib, ← Finset.mul_sum]
715 simp only [← minkowskiDot_eq_sum]
716 rw [hl0]
717 field_simp [hs0]; ring
718
719theorem sum_nullPMixed_raise_l (m l : Fin 4 → ℝ)
720 (hl0 : minkowskiDot l l = 0) (hml : minkowskiDot m l ≠ 0)
721 (b : Fin 4) :
722 (∑ j : Fin 4, nullPMixed m l j b * raise l j) = 0 := by
723 unfold nullPMixed
724 simp only [sub_mul, Finset.sum_sub_distrib]
725 have hδ : (∑ j : Fin 4, kron j b * raise l j) = raise l b := by
726 have : ∀ j, kron j b = kron b j := by
727 intro j; unfold kron; simp [eq_comm]
728 simp_rw [this]
729 exact sum_kron_left b (raise l)
730 rw [hδ, sum_nullSMixed_raise_l m l hl0 hml b]
731 ring
732
733theorem nullPhp_lorentzLoad_m (m l : Fin 4 → ℝ) (H : Mat4)
734 (hm0 : minkowskiDot m m = 0) (hml : minkowskiDot m l ≠ 0)
735 (i : Fin 4) :
736 lorentzLoad (nullPhp m l H) m i = 0 := by
737 unfold lorentzLoad nullPhp
738 have hswap :
739 (∑ j : Fin 4,
740 (∑ a : Fin 4, ∑ b : Fin 4,
741 nullPMixed m l i a * H a b * nullPMixed m l j b) * raise m j) =
742 ∑ a : Fin 4, ∑ b : Fin 4,
743 nullPMixed m l i a * H a b *
744 (∑ j : Fin 4, nullPMixed m l j b * raise m j) := by
745 simp_rw [Finset.sum_mul, Finset.mul_sum, mul_assoc]
746 rw [Finset.sum_comm]
747 exact Finset.sum_congr rfl fun a _ => Finset.sum_comm
748 rw [hswap]
749 refine Finset.sum_eq_zero fun a _ => Finset.sum_eq_zero fun b _ => ?_
750 simp [sum_nullPMixed_raise_m m l hm0 hml b]
751
752theorem nullPhp_transverse_m (m l : Fin 4 → ℝ) (H : Mat4)
753 (hm0 : minkowskiDot m m = 0) (hml : minkowskiDot m l ≠ 0) :
754 IsLorentzTransverse m (nullPhp m l H) := by
755 intro i
756 rw [← lorentzLoad_eq]
757 exact nullPhp_lorentzLoad_m m l H hm0 hml i
758
759theorem nullPhp_lorentzLoad_l (m l : Fin 4 → ℝ) (H : Mat4)
760 (hl0 : minkowskiDot l l = 0) (hml : minkowskiDot m l ≠ 0)
761 (i : Fin 4) :
762 lorentzLoad (nullPhp m l H) l i = 0 := by
763 unfold lorentzLoad nullPhp
764 have hswap :
765 (∑ j : Fin 4,
766 (∑ a : Fin 4, ∑ b : Fin 4,
767 nullPMixed m l i a * H a b * nullPMixed m l j b) * raise l j) =
768 ∑ a : Fin 4, ∑ b : Fin 4,
769 nullPMixed m l i a * H a b *
770 (∑ j : Fin 4, nullPMixed m l j b * raise l j) := by
771 simp_rw [Finset.sum_mul, Finset.mul_sum, mul_assoc]
772 rw [Finset.sum_comm]
773 exact Finset.sum_congr rfl fun a _ => Finset.sum_comm
774 rw [hswap]
775 refine Finset.sum_eq_zero fun a _ => Finset.sum_eq_zero fun b _ => ?_
776 simp [sum_nullPMixed_raise_l m l hl0 hml b]
777
778theorem nullPhp_transverse_l (m l : Fin 4 → ℝ) (H : Mat4)
779 (hl0 : minkowskiDot l l = 0) (hml : minkowskiDot m l ≠ 0) :
780 IsLorentzTransverse l (nullPhp m l H) := by
781 intro i
782 rw [← lorentzLoad_eq]
783 exact nullPhp_lorentzLoad_l m l H hl0 hml i
784
785theorem nullTTProject_symmetric (m l : Fin 4 → ℝ) (H : Mat4)
786 (hH : IsSymmetric H) :
787 IsSymmetric (nullTTProject m l H) := by
788 intro i j
789 simp only [nullTTProject, sub_apply, smul_apply, smul_eq_mul]
790 rw [nullPhp_symmetric m l H hH i j, nullProjector_symmetric m l i j]
791
792theorem nullTTProject_traceless (m l : Fin 4 → ℝ) (H : Mat4)
793 (hml : minkowskiDot m l ≠ 0) :
794 IsLorentzTraceless (nullTTProject m l H) := by
795 unfold IsLorentzTraceless nullTTProject nullTraceCoeff
796 rw [minkowskiTrace_sub, minkowskiTrace_smul,
797 nullProjector_minkowskiTrace m l hml]
798 ring
799
800theorem nullTTProject_transverse_m (m l : Fin 4 → ℝ) (H : Mat4)
801 (hm0 : minkowskiDot m m = 0) (hml : minkowskiDot m l ≠ 0) :
802 IsLorentzTransverse m (nullTTProject m l H) := by
803 intro i
804 rw [← lorentzLoad_eq]
805 have h1 := nullPhp_lorentzLoad_m m l H hm0 hml i
806 have h2 := lorentzLoad_nullProjector_m m l hm0 hml i
807 simp [nullTTProject, lorentzLoad_sub, lorentzLoad_smul, h1, h2]
808
809theorem nullTTProject_transverse_l (m l : Fin 4 → ℝ) (H : Mat4)
810 (hl0 : minkowskiDot l l = 0) (hml : minkowskiDot m l ≠ 0) :
811 IsLorentzTransverse l (nullTTProject m l H) := by
812 intro i
813 rw [← lorentzLoad_eq]
814 have h1 := nullPhp_lorentzLoad_l m l H hl0 hml i
815 have h2 := lorentzLoad_nullProjector_l m l hl0 hml i
816 simp [nullTTProject, lorentzLoad_sub, lorentzLoad_smul, h1, h2]
817
818theorem nullTTProject_isLorentzTT (m l : Fin 4 → ℝ) (H : Mat4)
819 (hH : IsSymmetric H) (hm0 : minkowskiDot m m = 0)
820 (hml : minkowskiDot m l ≠ 0) :
821 IsLorentzTT m (nullTTProject m l H) :=
822 ⟨nullTTProject_symmetric m l H hH, nullTTProject_traceless m l H hml,
823 nullTTProject_transverse_m m l H hm0 hml⟩
824
825/-- **THEOREM (null Lorentzian algebraic `edge_tt_decomposition`).**
826Explicit residual identity against a null wave covector with auxiliary null
827partner: TT + m-gauge + l-gauge − bilinear + screen-trace part. -/
828theorem exists_nullLorentzTTDecomposition (m l : Fin 4 → ℝ) (H : Mat4)
829 (hH : IsSymmetric H) (hm0 : minkowskiDot m m = 0)
830 (hl0 : minkowskiDot l l = 0) (hml : minkowskiDot m l ≠ 0) :
831 H =
832 nullTTProject m l H +
833 gaugePart m (nullMGaugeVector m l H) +
834 gaugePart l (nullLGaugeVector m l H) -
835 nullBilinear m l H +
836 nullTraceCoeff m l H • nullProjector m l ∧
837 IsLorentzTT m (nullTTProject m l H) ∧
838 IsLorentzTransverse l (nullTTProject m l H) := by
839 refine ⟨?_, nullTTProject_isLorentzTT m l H hH hm0 hml,
840 nullTTProject_transverse_l m l H hl0 hml⟩
841 have hgap := null_gap_expansion m l H hH hml
842 -- H = PHP + (gauge_m + gauge_l - bilinear)
843 -- = TT + trCoeff • P + (gauge_m + gauge_l - bilinear)
844 calc
845 H = nullPhp m l H + nullGap m l H := hgap
846 _ = nullPhp m l H +
847 (gaugePart m (nullMGaugeVector m l H) +
848 gaugePart l (nullLGaugeVector m l H) -
849 nullBilinear m l H) := by
850 rfl
851 _ = (nullPhp m l H - nullTraceCoeff m l H • nullProjector m l) +
852 gaugePart m (nullMGaugeVector m l H) +
853 gaugePart l (nullLGaugeVector m l H) -
854 nullBilinear m l H +
855 nullTraceCoeff m l H • nullProjector m l := by
856 abel
857 _ = nullTTProject m l H +
858 gaugePart m (nullMGaugeVector m l H) +
859 gaugePart l (nullLGaugeVector m l H) -
860 nullBilinear m l H +
861 nullTraceCoeff m l H • nullProjector m l := by
862 rfl
863
864/-! ## §4. Axis null witness: two independent TT polarizations -/
865
866def nullAxisWave : Fin 4 → ℝ := vec4 1 1 0 0
867def nullAxisAux : Fin 4 → ℝ := vec4 1 (-1) 0 0
868
869theorem nullAxisWave_dot : minkowskiDot nullAxisWave nullAxisWave = 0 := by
870 unfold minkowskiDot nullAxisWave; simp [vec4]
871
872theorem nullAxisAux_dot : minkowskiDot nullAxisAux nullAxisAux = 0 := by
873 unfold minkowskiDot nullAxisAux; simp [vec4]
874
875theorem nullAxis_cross_dot : minkowskiDot nullAxisWave nullAxisAux = -2 := by
876 unfold minkowskiDot nullAxisWave nullAxisAux; simp [vec4]; norm_num
877
878theorem nullAxisWave_ne_zero : nullAxisWave ≠ 0 := by
879 intro h
880 have := congrArg (fun v : Fin 4 → ℝ => v 0) h
881 simp [nullAxisWave, vec4] at this
882
883theorem nullAxis_MinkowskiNull :
884 MinkowskiNull nullAxisWave :=
885 (minkowskiDot_eq_MinkowskiNull nullAxisWave).mp nullAxisWave_dot
886
887/-- Plus polarization `diag(0,0,1,−1)` (unnormalized). -/
888def nullAxisTTPlus : Mat4
889 | 0, 0 => 0 | 0, 1 => 0 | 0, 2 => 0 | 0, 3 => 0
890 | 1, 0 => 0 | 1, 1 => 0 | 1, 2 => 0 | 1, 3 => 0
891 | 2, 0 => 0 | 2, 1 => 0 | 2, 2 => 1 | 2, 3 => 0
892 | 3, 0 => 0 | 3, 1 => 0 | 3, 2 => 0 | 3, 3 => -1
893
894/-- Cross polarization `H₂₃ = H₃₂ = 1` (unnormalized). -/
895def nullAxisTTCross : Mat4
896 | 0, 0 => 0 | 0, 1 => 0 | 0, 2 => 0 | 0, 3 => 0
897 | 1, 0 => 0 | 1, 1 => 0 | 1, 2 => 0 | 1, 3 => 0
898 | 2, 0 => 0 | 2, 1 => 0 | 2, 2 => 0 | 2, 3 => 1
899 | 3, 0 => 0 | 3, 1 => 0 | 3, 2 => 1 | 3, 3 => 0
900
901theorem nullAxisTTPlus_isLorentzTT :
902 IsLorentzTT nullAxisWave nullAxisTTPlus := by
903 refine ⟨?_, ?_, ?_⟩
904 · intro i j; fin_cases i <;> fin_cases j <;> rfl
905 · unfold IsLorentzTraceless minkowskiTrace nullAxisTTPlus; norm_num
906 · intro i
907 fin_cases i <;> simp [nullAxisTTPlus, nullAxisWave, vec4]
908
909theorem nullAxisTTCross_isLorentzTT :
910 IsLorentzTT nullAxisWave nullAxisTTCross := by
911 refine ⟨?_, ?_, ?_⟩
912 · intro i j; fin_cases i <;> fin_cases j <;> rfl
913 · unfold IsLorentzTraceless minkowskiTrace nullAxisTTCross; norm_num
914 · intro i
915 fin_cases i <;> simp [nullAxisTTCross, nullAxisWave, vec4]
916
917theorem nullAxisTTPlus_ne_zero : nullAxisTTPlus ≠ 0 := by
918 intro h
919 have := congrArg (fun M : Mat4 => M 2 2) h
920 simp [nullAxisTTPlus] at this
921
922theorem nullAxisTTCross_ne_zero : nullAxisTTCross ≠ 0 := by
923 intro h
924 have := congrArg (fun M : Mat4 => M 2 3) h
925 simp [nullAxisTTCross] at this
926
927theorem nullAxisTT_independent {a b : ℝ}
928 (h : a • nullAxisTTPlus + b • nullAxisTTCross = 0) :
929 a = 0 ∧ b = 0 := by
930 have h22 := congrArg (fun M : Mat4 => M 2 2) h
931 have h23 := congrArg (fun M : Mat4 => M 2 3) h
932 simp [nullAxisTTPlus, nullAxisTTCross, smul_eq_mul] at h22 h23
933 exact ⟨h22, h23⟩
934
935/-! ## §5. Decoys: Euclidean projector fails on the null cone; zero degeneracy -/
936
937/-- Euclidean momentum squared (for the decoy comparison only). -/
938def euclideanMomentumSq (m : Fin 4 → ℝ) : ℝ :=
939 ∑ i : Fin 4, m i * m i
940
941def euclideanTransverseProjector (m : Fin 4 → ℝ) : Mat4 :=
942 (1 : Mat4) - (euclideanMomentumSq m)⁻¹ • outerSq m
943
944theorem nullAxis_euclideanMomentumSq :
945 euclideanMomentumSq nullAxisWave = 2 := by
946 unfold euclideanMomentumSq nullAxisWave
947 simp [Fin.sum_univ_four, vec4]; norm_num
948
949theorem lorentzLoad_one (m : Fin 4 → ℝ) (i : Fin 4) :
950 lorentzLoad (1 : Mat4) m i = raise m i := by
951 unfold lorentzLoad
952 simp only [one_apply]
953 rw [Finset.sum_eq_single (a := i)]
954 · simp
955 · intro j _ hj; simp [Ne.symm hj]
956 · intro hi; exact (hi (Finset.mem_univ i)).elim
957
958/-- The Euclidean projector is defined on the null axis (`‖m‖²_E = 2 ≠ 0`),
959but it is **not** Lorentz-transverse to that null wave covector. -/
960theorem euclideanProjector_not_lorentzTransverse_on_nullAxis :
961 ¬ IsLorentzTransverse nullAxisWave
962 (euclideanTransverseProjector nullAxisWave) := by
963 intro h
964 have hL := (IsLorentzTransverse_iff_lorentzLoad _ _).mp h 0
965 have key :
966 lorentzLoad (euclideanTransverseProjector nullAxisWave) nullAxisWave 0 =
967 raise nullAxisWave 0 := by
968 unfold euclideanTransverseProjector
969 rw [lorentzLoad_sub, lorentzLoad_one, lorentzLoad_smul, lorentzLoad_outerSq,
970 nullAxisWave_dot]
971 simp [raise, nullAxisWave, vec4]
972 rw [key] at hL
973 simp [raise, nullAxisWave, vec4] at hL
974
975/-- Naive non-null Lorentz projector hypothesis fails on the null cone. -/
976theorem naive_lorentz_projector_hypothesis_fails_on_nullAxis :
977 ¬ (minkowskiDot nullAxisWave nullAxisWave ≠ 0) := by
978 simp [nullAxisWave_dot]
979
980theorem zero_wave_minkowskiDot :
981 minkowskiDot (fun _ : Fin 4 => (0 : ℝ)) (fun _ => 0) = 0 := by
982 unfold minkowskiDot; simp
983
984theorem decomposition_hypothesis_fails_at_zero :
985 ¬ (minkowskiDot (fun _ : Fin 4 => (0 : ℝ)) (fun _ => 0) ≠ 0) := by
986 simp [zero_wave_minkowskiDot]
987
988end
989
990end EdgeTTDecompositionLorentz4D
991end Analysis
992end Gravity
993end IndisputableMonolith
994