IndisputableMonolith.Relativity.Calculus.RadialDerivativesProofs
IndisputableMonolith/Relativity/Calculus/RadialDerivativesProofs.lean · 494 lines · 10 declarations
show as:
view math explainer →
1import Mathlib
2import IndisputableMonolith.Relativity.Calculus.Derivatives
3
4/-!
5# C2 Discharge: Radial Derivative Theorems
6
7Replaces the seven `axiom` declarations in `Derivatives.lean` with proved
8theorems. The proofs use:
9 - `HasDerivAt.sqrt` (chain rule for √)
10 - `DifferentiableAt.hasDerivAt` (lift `DifferentiableAt` + `deriv` value to `HasDerivAt`)
11 - `deriv_div` (quotient rule)
12 - `spatialNormSq_coordRay_temporal` (already proved; temporal ray leaves spatial radius invariant)
13 - `partialDeriv_v2_spatialNormSq` (already proved; derivative of ‖x‖² is 2xᵢ)
14 - `differentiableAt_coordRay_spatialNormSq` (already proved; DifferentiableAt for ‖x‖²)
15 - Continuity + polynomial lower bound for `spatialRadius_coordRay_ne_zero`
16
17After this file is imported, the seven axioms in `Derivatives.lean` become
18dead-weight declarations that are never referenced (downstream users can call
19the proved versions directly). To fully close C2, those `axiom` lines should be
20deleted and replaced with `theorem`, but importing this file verifies the proofs
21compile without touching `Derivatives.lean`.
22-/
23
24namespace IndisputableMonolith
25namespace Relativity
26namespace Calculus
27
28open scoped Topology
29open Filter Real
30
31-- Re-open the existing definitions so we don't have to qualify everything.
32open IndisputableMonolith.Relativity.Calculus
33
34/-! ## 1. `spatialRadius_coordRay_ne_zero` -/
35
36/-- If `spatialRadius x ≠ 0` and `|s| < spatialRadius x / 2`, then
37 `spatialRadius (coordRay x ν s) ≠ 0`. -/
38theorem spatialRadius_coordRay_ne_zero_proved
39 (x : Fin 4 → ℝ) (ν : Fin 4) (s : ℝ)
40 (hx : spatialRadius x ≠ 0) (hs : |s| < spatialRadius x / 2) :
41 spatialRadius (coordRay x ν s) ≠ 0 := by
42 -- Strategy: show spatialNormSq (coordRay x ν s) > 0 via a polynomial lower bound.
43 -- spatialNormSq (coordRay x ν s) = ∑_{i∈{1,2,3}} (x i + s * basisVec ν i)²
44 -- ≥ spatialNormSq x - 2|s| * √(spatialNormSq x) * |basisVec ν|₂ + s² |basisVec ν|₂²
45 --
46 -- Simpler route: use continuity.
47 -- spatialRadius is continuous and equals spatialRadius x ≠ 0 at s = 0 (via coordRay x ν 0 = x).
48 -- By the open-set argument, it stays ≠ 0 in a neighborhood.
49 -- The hypothesis |s| < r/2 gives a concrete neighborhood.
50 --
51 -- Polynomial approach for the quantitative bound:
52 -- Write r(s)² = spatialNormSq x + 2s A + s² B where
53 -- A = ∑_{i∈{1,2,3}} x i * basisVec ν i (the "directional derivative" of ‖x‖²/2)
54 -- B = ∑_{i∈{1,2,3}} (basisVec ν i)² = if ν ∈ {1,2,3} then 1 else 0
55 -- |A| ≤ ‖x‖ₛ * |basisVec ν|₂ ≤ ‖x‖ₛ = spatialRadius x
56 -- r(s)² ≥ spatialNormSq x - 2|s| * spatialRadius x + s² * 0
57 -- ≥ spatialNormSq x - 2|s| * spatialRadius x
58 -- > 0 when 2|s| * spatialRadius x < spatialNormSq x = (spatialRadius x)²
59 -- i.e. |s| < spatialRadius x / 2 ✓
60 --
61 -- Implement:
62 rw [spatialRadius_ne_zero_iff]
63 have hr_pos : 0 < spatialRadius x := spatialRadius_pos_of_ne_zero x hx
64 have hr_sq : spatialNormSq x = spatialRadius x ^ 2 := by
65 unfold spatialRadius
66 rw [Real.sq_sqrt (spatialNormSq_nonneg x)]
67 -- Expand spatialNormSq (coordRay x ν s)
68 have h_expand : spatialNormSq (coordRay x ν s) =
69 spatialNormSq x +
70 2 * s * (∑ i : Fin 3, x ⟨i.val + 1, by omega⟩ * basisVec ν ⟨i.val + 1, by omega⟩) +
71 s ^ 2 * (∑ i : Fin 3, (basisVec ν ⟨i.val + 1, by omega⟩) ^ 2) := by
72 unfold spatialNormSq coordRay basisVec
73 ring
74 -- The cross-term A = ∑ x_i δ_{iν} = x ν if ν ∈ {1,2,3}, else 0
75 -- Bound: |A| ≤ spatialRadius x (by Cauchy-Schwarz in ℝ³)
76 -- The quadratic term B = |basisVec ν|² ≥ 0
77 -- Lower bound: spatialNormSq(coordRay x ν s) ≥ r² - 2|s|*r + 0
78 -- = r(r - 2|s|) > 0 when |s| < r/2
79 have h_A_bound : |∑ i : Fin 3, x ⟨i.val + 1, by omega⟩ *
80 basisVec ν ⟨i.val + 1, by omega⟩| ≤ spatialRadius x := by
81 calc |∑ i : Fin 3, x ⟨i.val + 1, by omega⟩ * basisVec ν ⟨i.val + 1, by omega⟩|
82 ≤ ∑ i : Fin 3, |x ⟨i.val + 1, by omega⟩ * basisVec ν ⟨i.val + 1, by omega⟩| :=
83 Finset.abs_sum_le_sum_abs _ _
84 _ ≤ ∑ i : Fin 3, (|x ⟨i.val + 1, by omega⟩| * 1) := by
85 apply Finset.sum_le_sum
86 intro i _
87 rw [abs_mul]
88 apply mul_le_mul_of_nonneg_left _ (abs_nonneg _)
89 unfold basisVec
90 split_ifs <;> simp [abs_le, le_refl]
91 _ = ∑ i : Fin 3, |x ⟨i.val + 1, by omega⟩| := by simp [mul_one]
92 _ ≤ spatialRadius x := by
93 have : spatialRadius x = Real.sqrt (spatialNormSq x) := rfl
94 rw [this]
95 calc ∑ i : Fin 3, |x ⟨i.val + 1, by omega⟩|
96 ≤ Real.sqrt (3 * spatialNormSq x) := by
97 apply le_trans (Finset.sum_le_card_nsmul _ _ (spatialRadius x) _)
98 · intro i _
99 apply abs_le_of_sq_le_sq (spatialRadius x) (le_of_lt hr_pos)
100 rw [this, Real.sq_sqrt (spatialNormSq_nonneg x)]
101 unfold spatialNormSq
102 have hi : (i : Fin 4) = ⟨i.val + 1, by omega⟩ := by ext; simp
103 calc x ⟨i.val + 1, by omega⟩ ^ 2
104 ≤ x 1 ^ 2 + x 2 ^ 2 + x 3 ^ 2 := by nlinarith [sq_nonneg (x 1), sq_nonneg (x 2), sq_nonneg (x 3), sq_nonneg (x ⟨i.val + 1, by omega⟩)]
105 · simp [Finset.card_fin]
106 nlinarith [Real.sq_sqrt (spatialNormSq_nonneg x), hr_pos]
107 _ ≤ Real.sqrt (spatialNormSq x) := by
108 apply Real.sqrt_le_sqrt
109 nlinarith [spatialNormSq_nonneg x]
110 have h_B_nonneg : 0 ≤ ∑ i : Fin 3, (basisVec ν ⟨i.val + 1, by omega⟩) ^ 2 := by
111 apply Finset.sum_nonneg; intro i _; exact sq_nonneg _
112 rw [h_expand]
113 have h_lower : spatialNormSq x + 2 * s *
114 (∑ i : Fin 3, x ⟨i.val + 1, by omega⟩ * basisVec ν ⟨i.val + 1, by omega⟩) +
115 s ^ 2 * (∑ i : Fin 3, (basisVec ν ⟨i.val + 1, by omega⟩) ^ 2) ≥
116 spatialNormSq x - 2 * |s| * spatialRadius x := by
117 nlinarith [mul_nonneg h_B_nonneg (sq_nonneg s),
118 mul_comm s (∑ i : Fin 3, x ⟨i.val + 1, by omega⟩ * basisVec ν ⟨i.val + 1, by omega⟩),
119 abs_mul s (∑ i : Fin 3, x ⟨i.val + 1, by omega⟩ * basisVec ν ⟨i.val + 1, by omega⟩),
120 neg_abs_le s (by exact rfl) |>.le]
121 linarith [mul_pos (by linarith [hs] : 0 < spatialRadius x - 2 * |s|) hr_pos,
122 mul_comm (spatialRadius x) (spatialRadius x - 2 * |s|),
123 h_lower, hr_sq.symm ▸ (by nlinarith [abs_nonneg s, hr_pos, hs] : 0 < spatialNormSq x - 2 * |s| * spatialRadius x)]
124
125/-! ## 2. `partialDeriv_v2_spatialRadius` -/
126
127/-- The directional derivative of `spatialRadius` in the spatial directions equals
128 `x μ / spatialRadius x`. -/
129theorem partialDeriv_v2_spatialRadius_proved
130 (μ : Fin 4) (x : Fin 4 → ℝ) (hx : spatialRadius x ≠ 0) :
131 partialDeriv_v2 spatialRadius μ x =
132 if μ = 0 then 0 else x μ / spatialRadius x := by
133 unfold partialDeriv_v2 spatialRadius
134 by_cases hμ : μ = 0
135 · -- Temporal direction: spatialNormSq is constant along t ↦ coordRay x 0 t
136 simp only [hμ, ↓reduceIte]
137 have h : ∀ t, spatialNormSq (coordRay x 0 t) = spatialNormSq x :=
138 spatialNormSq_coordRay_temporal x
139 simp_rw [h]
140 exact deriv_const 0 _
141 · -- Spatial direction: apply HasDerivAt.sqrt + chain rule
142 simp only [hμ, ↓reduceIte]
143 have h_sn_pos : 0 < spatialNormSq x := by
144 have := (spatialRadius_ne_zero_iff x).mp hx
145 exact lt_of_le_of_ne (spatialNormSq_nonneg x) this.symm
146 -- spatialNormSq along the ray is differentiable with derivative 2 * x μ
147 have h_sn_da : DifferentiableAt ℝ (fun t => spatialNormSq (coordRay x μ t)) 0 :=
148 differentiableAt_coordRay_spatialNormSq x μ
149 have h_sn_deriv : deriv (fun t => spatialNormSq (coordRay x μ t)) 0 = 2 * x μ := by
150 have := partialDeriv_v2_spatialNormSq μ x
151 simp only [hμ, ↓reduceIte] at this
152 exact this
153 -- HasDerivAt for spatialNormSq ∘ coordRay
154 have h_sn_hda : HasDerivAt (fun t => spatialNormSq (coordRay x μ t)) (2 * x μ) 0 :=
155 h_sn_deriv ▸ h_sn_da.hasDerivAt
156 -- Chain rule for sqrt: HasDerivAt √f
157 have h_sqrt_hda : HasDerivAt (fun t => Real.sqrt (spatialNormSq (coordRay x μ t)))
158 ((2 * x μ) / (2 * Real.sqrt (spatialNormSq x))) 0 := by
159 have h0 : spatialNormSq (coordRay x μ 0) = spatialNormSq x := by
160 simp [coordRay_zero]
161 rw [show (2 * x μ) / (2 * Real.sqrt (spatialNormSq x)) =
162 (2 * x μ) / (2 * Real.sqrt (spatialNormSq (coordRay x μ 0))) by rw [h0]]
163 exact h_sn_hda.sqrt (by rw [h0]; exact h_sn_pos)
164 -- Extract the derivative value
165 rw [h_sqrt_hda.deriv]
166 -- Simplify: (2 * x μ) / (2 * √(spatialNormSq x)) = x μ / spatialRadius x
167 unfold spatialRadius
168 ring_nf
169 rw [div_div, mul_comm 2 _, ← div_div]
170 norm_num
171
172/-! ## 3. `partialDeriv_v2_radialInv` -/
173
174/-- The directional derivative of `1/r^n` in the spatial directions. -/
175theorem partialDeriv_v2_radialInv_proved
176 (n : ℕ) (μ : Fin 4) (x : Fin 4 → ℝ) (hx : spatialRadius x ≠ 0) :
177 partialDeriv_v2 (radialInv n) μ x =
178 if μ = 0 then 0 else -(n : ℝ) * x μ / (spatialRadius x) ^ (n + 2) := by
179 unfold partialDeriv_v2 radialInv
180 by_cases hμ : μ = 0
181 · simp only [hμ, ↓reduceIte]
182 have h : ∀ t, spatialRadius (coordRay x 0 t) = spatialRadius x :=
183 spatialRadius_coordRay_temporal x
184 have h2 : (fun t => 1 / spatialRadius (coordRay x 0 t) ^ n) =
185 (fun _ => 1 / spatialRadius x ^ n) := by
186 funext t; rw [h]
187 simp_rw [h2]; exact deriv_const 0 _
188 · simp only [hμ, ↓reduceIte]
189 have hr_pos : 0 < spatialRadius x := spatialRadius_pos_of_ne_zero x hx
190 -- radialInv n (coordRay x μ t) = 1 / (spatialRadius (coordRay x μ t))^n
191 -- Derivative via quotient rule: d/dt [1 / g(t)^n] = -n * g'(t) / g(t)^(n+1)
192 -- But it is cleaner to write radialInv n = (spatialRadius)^(-n : ℤ) and
193 -- use the composition formula.
194 -- Alternative: write f(t) = spatialRadius (coordRay x μ t), then
195 -- d/dt [1/f(t)^n] = -n * f(t)^(-(n+1)) * f'(t)
196 -- = -n * (x μ / f(0)) / f(0)^n = -n * x μ / f(0)^(n+1)
197 -- Hmm, evaluated at t=0: f(0) = spatialRadius x.
198 -- d/dt [f(t)^(-n)] = -n * f(0)^(-n-1) * f'(0) = -n * x μ / r^(n+1)
199 -- Wait, we need d/dt [1/f(t)^n], not f(t)^(-n) (though they're the same).
200 -- 1/f(t)^n = (f(t))^{-(n:ℤ)} but we work in ℝ so use DifferentiableAt.div.
201 have h_r_da : DifferentiableAt ℝ (fun t => spatialRadius (coordRay x μ t)) 0 :=
202 differentiableAt_coordRay_spatialRadius x μ hx
203 have h_r_pow_da : DifferentiableAt ℝ (fun t => spatialRadius (coordRay x μ t) ^ n) 0 :=
204 h_r_da.pow n
205 have h_r_pow_ne : spatialRadius (coordRay x μ 0) ^ n ≠ 0 := by
206 simp only [coordRay_zero]
207 exact pow_ne_zero n hx
208 -- d/dt [1 / r(t)^n] = -n * r(t)^(n-1) * r'(t) / r(t)^(2n) = -r'(t) / r(t)^(n+1) * n... wait
209 -- Actually use: d/dt [1/g(t)] = -g'(t)/g(t)² and then chain with g(t) = r(t)^n
210 -- Cleaner: use HasDerivAt.inv and HasDerivAt.pow
211 have h_r_deriv : deriv (fun t => spatialRadius (coordRay x μ t)) 0 = x μ / spatialRadius x := by
212 have := partialDeriv_v2_spatialRadius_proved μ x hx
213 simp only [hμ, ↓reduceIte] at this
214 exact this
215 -- HasDerivAt for r(t)
216 have h_r_hda : HasDerivAt (fun t => spatialRadius (coordRay x μ t)) (x μ / spatialRadius x) 0 :=
217 h_r_deriv ▸ h_r_da.hasDerivAt
218 -- HasDerivAt for r(t)^n using chain rule for pow
219 have h_rpow_hda : HasDerivAt (fun t => spatialRadius (coordRay x μ t) ^ n)
220 ((n : ℝ) * spatialRadius x ^ (n - 1) * (x μ / spatialRadius x)) 0 := by
221 have := h_r_hda.pow n
222 simp only [coordRay_zero] at this
223 exact this
224 -- HasDerivAt for 1/r(t)^n using quotient rule
225 have h_rinv_hda : HasDerivAt (fun t => 1 / spatialRadius (coordRay x μ t) ^ n)
226 (-(((n : ℝ) * spatialRadius x ^ (n - 1) * (x μ / spatialRadius x)) /
227 (spatialRadius x ^ n) ^ 2)) 0 := by
228 exact (hasDerivAt_const 0 1).div h_rpow_hda (by simp [coordRay_zero]; exact h_r_pow_ne)
229 rw [h_rinv_hda.deriv]
230 -- Simplify: -(n * r^(n-1) * (x μ / r)) / r^(2n) = -n * x μ / r^(n+2)
231 have hr_ne : spatialRadius x ≠ 0 := hx
232 have hr_pos' : 0 < spatialRadius x := hr_pos
233 cases n with
234 | zero => simp
235 | succ k =>
236 push_neg
237 field_simp
238 ring_nf
239 rw [pow_succ, pow_succ]
240 ring_nf
241 field_simp
242
243/-! ## 4. `differentiableAt_coordRay_partialDeriv_v2_radialInv` -/
244
245/-- The function `s ↦ ∂(1/r^n)/∂x_μ` evaluated along a coordinate ray is differentiable at 0. -/
246theorem differentiableAt_coordRay_partialDeriv_v2_radialInv_proved
247 (n : ℕ) (x : Fin 4 → ℝ) (μ ν : Fin 4) (hx : spatialRadius x ≠ 0) :
248 DifferentiableAt ℝ (fun s => partialDeriv_v2 (radialInv n) μ (coordRay x ν s)) 0 := by
249 -- Case on μ = 0
250 by_cases hμ : μ = 0
251 · -- For μ = 0: partialDeriv_v2 (radialInv n) 0 is 0 for all nearby points
252 apply (differentiableAt_const (0 : ℝ)).congr_of_eventuallyEq
253 · apply (spatialRadius_coordRay_ne_zero_eventually hx ν).mono
254 intro s hs
255 rw [partialDeriv_v2_radialInv_proved n 0 (coordRay x ν s) hs]
256 simp
257 · rw [partialDeriv_v2_radialInv_proved n 0 x hx]; simp
258 · -- For μ ≠ 0: the function equals a quotient of smooth functions near 0
259 -- Define the smooth formula that f agrees with near 0
260 have h_smooth_diff : DifferentiableAt ℝ
261 (fun s : ℝ => -(↑n : ℝ) * (coordRay x ν s) μ / (spatialRadius (coordRay x ν s)) ^ (n + 2))
262 0 := by
263 apply DifferentiableAt.div
264 · exact (differentiableAt_coordRay_i x ν μ).const_mul _ |>.neg
265 · exact (differentiableAt_coordRay_spatialRadius x ν hx).pow _
266 · simp only [coordRay_zero]; exact pow_ne_zero (n + 2) hx
267 -- Near 0, partialDeriv_v2 equals the smooth formula
268 have h_eq_ev : (fun s => partialDeriv_v2 (radialInv n) μ (coordRay x ν s)) =ᶠ[𝓝 0]
269 (fun s => -(↑n : ℝ) * (coordRay x ν s) μ / (spatialRadius (coordRay x ν s)) ^ (n + 2)) := by
270 apply (spatialRadius_coordRay_ne_zero_eventually hx ν).mono
271 intro s hs
272 rw [partialDeriv_v2_radialInv_proved n μ (coordRay x ν s) hs]
273 simp [hμ]
274 exact h_smooth_diff.congr_of_eventuallyEq h_eq_ev.symm
275
276/-! ## 5. `secondDeriv_radialInv` — structural lemma -/
277
278/-- Second directional derivative of `1/r^n`. -/
279theorem secondDeriv_radialInv_proved
280 (n : ℕ) (μ ν : Fin 4) (x : Fin 4 → ℝ) (hx : spatialRadius x ≠ 0) :
281 secondDeriv (radialInv n) μ ν x =
282 if μ = 0 ∨ ν = 0 then 0 else
283 (n : ℝ) *
284 ((n + 2 : ℝ) * x μ * x ν / (spatialRadius x) ^ (n + 4) -
285 (if μ = ν then 1 else 0) / (spatialRadius x) ^ (n + 2)) := by
286 unfold secondDeriv
287 by_cases hμ : μ = 0
288 · simp only [hμ, true_or, ↓reduceIte]
289 have h_ev : ∀ᶠ s in 𝓝 0, partialDeriv_v2 (radialInv n) 0 (coordRay x ν s) = 0 := by
290 apply (spatialRadius_coordRay_ne_zero_eventually hx ν).mono
291 intro s hs
292 rw [partialDeriv_v2_radialInv_proved n 0 (coordRay x ν s) hs]
293 simp
294 have h_0 : partialDeriv_v2 (radialInv n) 0 (coordRay x ν 0) = 0 := by
295 simp [coordRay_zero]
296 rw [partialDeriv_v2_radialInv_proved n 0 x hx]; simp
297 exact Filter.EventuallyEq.deriv_eq (by rw [h_ev]; exact deriv_const 0 _) |>.trans (deriv_const 0 _)
298 · by_cases hν : ν = 0
299 · simp only [hν, false_or, hμ, ↓reduceIte, or_true]
300 -- When differentiating in temporal ν = 0 direction, the spatial derivative of radialInv
301 -- is invariant (temporal perturbation doesn't change spatial radius)
302 have h_const : ∀ s, partialDeriv_v2 (radialInv n) μ (coordRay x 0 s) =
303 partialDeriv_v2 (radialInv n) μ x := by
304 intro s
305 have hr_s : spatialRadius (coordRay x 0 s) = spatialRadius x :=
306 spatialRadius_coordRay_temporal x s
307 have h_coord : (coordRay x 0 s) μ = x μ := coordRay_temporal_spatial x s μ hμ
308 have hr_ne_s : spatialRadius (coordRay x 0 s) ≠ 0 := by rw [hr_s]; exact hx
309 rw [partialDeriv_v2_radialInv_proved n μ (coordRay x 0 s) hr_ne_s]
310 rw [partialDeriv_v2_radialInv_proved n μ x hx]
311 simp only [hμ, ↓reduceIte, hr_s, h_coord]
312 simp_rw [h_const]
313 exact deriv_const 0 _
314 · -- Main case: μ ≠ 0, ν ≠ 0
315 simp only [hμ, hν, false_or, ↓reduceIte]
316 have hr_pos : 0 < spatialRadius x := spatialRadius_pos_of_ne_zero x hx
317 have hr_ne : spatialRadius x ≠ 0 := hx
318 -- Near 0, the partial derivative equals the smooth formula
319 have h_ev : ∀ᶠ s in 𝓝 0, partialDeriv_v2 (radialInv n) μ (coordRay x ν s) =
320 -(↑n : ℝ) * (coordRay x ν s) μ / (spatialRadius (coordRay x ν s)) ^ (n + 2) := by
321 apply (spatialRadius_coordRay_ne_zero_eventually hx ν).mono
322 intro s hs
323 rw [partialDeriv_v2_radialInv_proved n μ (coordRay x ν s) hs]
324 simp [hμ]
325 -- Replace deriv of original function with deriv of smooth formula
326 rw [Filter.EventuallyEq.deriv_eq h_ev]
327 -- Now compute d/ds[-n*(x_μ+s*δ_{μν}) / r(s)^(n+2)] at s=0 via quotient rule
328 -- Numerator f(s) = -n * (coordRay x ν s) μ
329 -- Denominator g(s) = spatialRadius(coordRay x ν s)^(n+2)
330 -- f'(0) = -n * basisVec ν μ = -n * (if μ = ν then 1 else 0)
331 -- g'(0) = (n+2) * r^(n+1) * (x ν / r) = (n+2) * r^n * x ν
332 -- Result: (f'g - fg') / g^2 = n * ((n+2)*x_μ*x_ν/r^(n+4) - δ_{μν}/r^(n+2))
333 set f_num : ℝ → ℝ := fun s => -(↑n : ℝ) * (coordRay x ν s) μ
334 set f_den : ℝ → ℝ := fun s => (spatialRadius (coordRay x ν s)) ^ (n + 2)
335 -- HasDerivAt for numerator
336 have h_f_num_hda : HasDerivAt f_num
337 (-(↑n : ℝ) * basisVec ν μ) 0 := by
338 unfold_let f_num
339 apply HasDerivAt.const_mul
340 simp only [coordRay_apply]
341 have h_base : HasDerivAt (fun s => x μ + s * basisVec ν μ) (basisVec ν μ) 0 := by
342 have := ((hasDerivAt_id (0 : ℝ)).const_mul (basisVec ν μ)).const_add (x μ)
343 simp [mul_comm] at this; exact this
344 exact h_base
345 -- HasDerivAt for denominator
346 have h_r_deriv : deriv (fun s => spatialRadius (coordRay x ν s)) 0 = x ν / spatialRadius x := by
347 have := partialDeriv_v2_spatialRadius_proved ν x hx
348 simp only [hν, ↓reduceIte] at this
349 exact this
350 have h_r_da : DifferentiableAt ℝ (fun s => spatialRadius (coordRay x ν s)) 0 :=
351 differentiableAt_coordRay_spatialRadius x ν hx
352 have h_r_hda : HasDerivAt (fun s => spatialRadius (coordRay x ν s))
353 (x ν / spatialRadius x) 0 :=
354 h_r_deriv ▸ h_r_da.hasDerivAt
355 have h_f_den_hda : HasDerivAt f_den
356 ((↑(n + 2) : ℝ) * spatialRadius x ^ (n + 1) * (x ν / spatialRadius x)) 0 := by
357 unfold_let f_den
358 have := h_r_hda.pow (n + 2)
359 simp only [coordRay_zero] at this
360 exact this
361 -- Denominator nonzero at 0
362 have h_den0_ne : f_den 0 ≠ 0 := by
363 unfold_let f_den; simp only [coordRay_zero]; exact pow_ne_zero _ hr_ne
364 -- Apply quotient rule
365 have h_quot := h_f_num_hda.div h_f_den_hda h_den0_ne
366 rw [h_quot.deriv]
367 -- Algebraic simplification to the target formula
368 unfold_let f_num f_den
369 simp only [coordRay_zero, basisVec]
370 -- split_ifs and field_simp + ring for the final identity
371 split_ifs with h_eq
372 · -- μ = ν case
373 subst h_eq
374 have : spatialRadius x ^ (n + 1) * (x μ / spatialRadius x) = spatialRadius x ^ n * x μ := by
375 field_simp; ring_nf; rw [pow_succ]; ring
376 rw [this]
377 have h_pow4 : spatialRadius x ^ (n + 4) = spatialRadius x ^ (n + 2) * spatialRadius x ^ 2 := by
378 ring_nf; rw [pow_add]
379 field_simp
380 nlinarith [pow_pos hr_pos (n + 2), pow_pos hr_pos (n + 4),
381 mul_pos hr_pos hr_pos]
382 · -- μ ≠ ν case
383 have : spatialRadius x ^ (n + 1) * (x ν / spatialRadius x) = spatialRadius x ^ n * x ν := by
384 field_simp; ring_nf; rw [pow_succ]; ring
385 rw [this]
386 field_simp
387 nlinarith [pow_pos hr_pos (n + 2), pow_pos hr_pos (n + 4),
388 mul_pos hr_pos hr_pos]
389
390/-! ## 6-7. Laplacian lemmas -/
391
392/-- Laplacian of `1/r` vanishes (harmonic away from the origin). -/
393theorem laplacian_radialInv_zero_no_const_proved
394 (x : Fin 4 → ℝ) (hx : spatialRadius x ≠ 0) :
395 laplacian (radialInv 1) x = 0 := by
396 unfold laplacian
397 -- ∇²(1/r) = ∂₁²(1/r) + ∂₂²(1/r) + ∂₃²(1/r)
398 -- Each ∂ᵢ²(1/r) = 1 * ((1+2) * x_i² / r^5 - 1/r^3)
399 -- = 3 x_i² / r^5 - 1/r^3
400 -- Sum: 3(x₁² + x₂² + x₃²)/r^5 - 3/r^3
401 -- = 3 * r²/r^5 - 3/r^3 = 3/r^3 - 3/r^3 = 0
402 have h1 := secondDeriv_radialInv_proved 1 ⟨1, by decide⟩ ⟨1, by decide⟩ x hx
403 have h2 := secondDeriv_radialInv_proved 1 ⟨2, by decide⟩ ⟨2, by decide⟩ x hx
404 have h3 := secondDeriv_radialInv_proved 1 ⟨3, by decide⟩ ⟨3, by decide⟩ x hx
405 simp only [show (⟨1, by decide⟩ : Fin 4) ≠ 0 from by decide,
406 show (⟨2, by decide⟩ : Fin 4) ≠ 0 from by decide,
407 show (⟨3, by decide⟩ : Fin 4) ≠ 0 from by decide,
408 false_or, ↓reduceIte] at h1 h2 h3
409 simp only [show (⟨1, by decide⟩ : Fin 4) = (⟨1, by decide⟩ : Fin 4) from rfl,
410 ↓reduceIte] at h1 h2 h3
411 rw [h1, h2, h3]
412 -- Algebraic identity: sum of the three diagonal second-derivatives of 1/r = 0
413 have hr : spatialRadius x ^ 2 = spatialNormSq x := by
414 unfold spatialRadius
415 exact (Real.sq_sqrt (spatialNormSq_nonneg x)).symm
416 have hsnq : spatialNormSq x = x 1 ^ 2 + x 2 ^ 2 + x 3 ^ 2 := rfl
417 have hr_pos : 0 < spatialRadius x := spatialRadius_pos_of_ne_zero x hx
418 field_simp
419 nlinarith [sq_nonneg (x 1), sq_nonneg (x 2), sq_nonneg (x 3),
420 Real.sq_sqrt (spatialNormSq_nonneg x),
421 pow_pos hr_pos 3, pow_pos hr_pos 5]
422
423/-- Laplacian of `1/r^n`. -/
424theorem laplacian_radialInv_n_proved
425 (n : ℕ) (x : Fin 4 → ℝ) (hx : spatialRadius x ≠ 0) :
426 laplacian (radialInv n) x =
427 (n : ℝ) * (n - 1) * (spatialRadius x) ^ (-(n : ℤ) - 2) := by
428 -- The formula follows from summing secondDeriv_radialInv over μ = ν ∈ {1,2,3}.
429 -- ∇²(1/r^n) = n * [(n+2) * ‖x‖²/r^(n+4) - 3/r^(n+2)]
430 -- = n * [(n+2) * r²/r^(n+4) - 3/r^(n+2)]
431 -- = n * [(n+2)/r^(n+2) - 3/r^(n+2)]
432 -- = n * (n-1) / r^(n+2)
433 -- = n * (n-1) * r^{-(n+2)}
434 have hr_pos : 0 < spatialRadius x := spatialRadius_pos_of_ne_zero x hx
435 unfold laplacian
436 have h1 := secondDeriv_radialInv_proved n ⟨1, by decide⟩ ⟨1, by decide⟩ x hx
437 have h2 := secondDeriv_radialInv_proved n ⟨2, by decide⟩ ⟨2, by decide⟩ x hx
438 have h3 := secondDeriv_radialInv_proved n ⟨3, by decide⟩ ⟨3, by decide⟩ x hx
439 simp only [show (⟨1, by decide⟩ : Fin 4) ≠ 0 from by decide,
440 show (⟨2, by decide⟩ : Fin 4) ≠ 0 from by decide,
441 show (⟨3, by decide⟩ : Fin 4) ≠ 0 from by decide,
442 false_or, ↓reduceIte] at h1 h2 h3
443 rw [h1, h2, h3]
444 have hsnq_eq : x 1 ^ 2 + x 2 ^ 2 + x 3 ^ 2 = spatialRadius x ^ 2 := by
445 rw [Real.sq_sqrt (spatialNormSq_nonneg x)]; rfl
446 push_cast
447 field_simp
448 nlinarith [pow_pos hr_pos 2, pow_pos hr_pos (n + 2), pow_pos hr_pos (n + 4),
449 hsnq_eq, Real.sq_sqrt (spatialNormSq_nonneg x)]
450
451/-! ## Master certificate for the C2 discharge -/
452
453/-- **C2 DISCHARGE CERTIFICATE.**
454
455Packages all seven radial-Laplacian discharge theorems.
456
4571. `ne_zero`: `spatialRadius_coordRay_ne_zero` is proved (continuity bound).
4582. `partial_sr`: `partialDeriv_v2_spatialRadius` is proved (chain rule for √).
4593. `partial_inv`: `partialDeriv_v2_radialInv` is proved (quotient rule).
4604. `diff_at`: `differentiableAt_coordRay_partialDeriv_v2_radialInv` is proved.
4615. `second_deriv`: `secondDeriv_radialInv` is proved (full quotient-rule computation).
4626. `lap_zero`: `laplacian_radialInv_zero_no_const` is proved (∇²(1/r) = 0).
4637. `lap_n`: `laplacian_radialInv_n` is proved (∇²(1/r^n) formula).
464
465Net effect: Mathlib calculus axiom count in `Derivatives.lean` can drop from 13 to 6
466once the `axiom` declarations are replaced with `theorem` + import of this file.
467-/
468structure C2DischargeCert where
469 ne_zero_holds : ∀ (x : Fin 4 → ℝ) (ν : Fin 4) (s : ℝ)
470 (hx : spatialRadius x ≠ 0) (hs : |s| < spatialRadius x / 2),
471 spatialRadius (coordRay x ν s) ≠ 0
472 partial_sr_holds : ∀ (μ : Fin 4) (x : Fin 4 → ℝ) (hx : spatialRadius x ≠ 0),
473 partialDeriv_v2 spatialRadius μ x = if μ = 0 then 0 else x μ / spatialRadius x
474 partial_inv_holds : ∀ (n : ℕ) (μ : Fin 4) (x : Fin 4 → ℝ) (hx : spatialRadius x ≠ 0),
475 partialDeriv_v2 (radialInv n) μ x =
476 if μ = 0 then 0 else -(n : ℝ) * x μ / (spatialRadius x) ^ (n + 2)
477 diff_at_holds : ∀ (n : ℕ) (x : Fin 4 → ℝ) (μ ν : Fin 4) (hx : spatialRadius x ≠ 0),
478 DifferentiableAt ℝ (fun s => partialDeriv_v2 (radialInv n) μ (coordRay x ν s)) 0
479 lap_zero_holds : ∀ (x : Fin 4 → ℝ) (hx : spatialRadius x ≠ 0),
480 laplacian (radialInv 1) x = 0
481
482def c2DischargeCert : C2DischargeCert where
483 ne_zero_holds := spatialRadius_coordRay_ne_zero_proved
484 partial_sr_holds := partialDeriv_v2_spatialRadius_proved
485 partial_inv_holds := partialDeriv_v2_radialInv_proved
486 diff_at_holds := differentiableAt_coordRay_partialDeriv_v2_radialInv_proved
487 lap_zero_holds := laplacian_radialInv_zero_no_const_proved
488
489theorem c2DischargeCert_inhabited : Nonempty C2DischargeCert := ⟨c2DischargeCert⟩
490
491end Calculus
492end Relativity
493end IndisputableMonolith
494