spatialRadius_coordRay_ne_zero_proved
The theorem shows that a coordinate-ray perturbation of a four-vector keeps the spatial radius nonzero whenever the original radius is nonzero and the step satisfies |s| < r/2. Researchers deriving radial derivatives or the Laplacian in relativistic models cite it to justify domain restrictions. The tactic proof expands the squared spatial norm to a quadratic in s, bounds the cross term by the original radius via absolute-value sums and a norm comparison, then applies nlinarith and linarith to obtain strict positivity.
claimLet $r(x)$ be the Euclidean norm of the three spatial components of the four-vector $x$. If $r(x) > 0$ and $|s| < r(x)/2$, then $r(x + s e_ν) > 0$, where $e_ν$ is the standard basis vector in coordinate direction $ν$ (vanishing on the time component).
background
The module replaces seven axiom declarations in Derivatives.lean with explicit theorems for radial derivatives. spatialRadius extracts the Euclidean length of the spatial part of a Fin 4 → ℝ vector; coordRay adds a scalar multiple of the corresponding basis vector. The local setting is the C2 discharge, which supplies the non-vanishing and differentiability facts needed for quotient and chain rules on expressions involving 1/spatialRadius and its Laplacian.
proof idea
The proof rewrites the goal via spatialRadius_ne_zero_iff, obtains positivity of the original radius, and expands spatialNormSq(coordRay x ν s) by ring into r² + 2s A + s² B. It bounds |A| ≤ r by summing absolutes, applying abs_mul, and comparing the sum of absolutes to the norm via a sqrt(3) estimate and nlinarith. B is shown nonnegative by sum_nonneg. A quadratic lower bound r² - 2|s|r is derived by nlinarith, then linarith closes positivity under the step-size hypothesis.
why it matters in Recognition Science
The result supplies the ne_zero_holds field of c2DischargeCert, which aggregates the proved radial facts and renders the original axioms in Derivatives.lean dead weight. It closes a key non-vanishing hypothesis required for the full C2 discharge in the relativity calculus. In the Recognition framework it supports differentiability steps that feed into mass formulas and phi-ladder constructions by keeping perturbed points inside the domain where spatial norms remain positive and differentiable.
scope and limits
- Does not establish differentiability of spatialRadius or its derivatives.
- Does not apply when |s| ≥ spatialRadius x / 2.
- Does not cover the case spatialRadius x = 0.
- Does not address temporal components or the full Minkowski norm.
- Does not supply an explicit positive lower bound on the perturbed radius.
Lean usage
def c2DischargeCert : C2DischargeCert where ne_zero_holds := spatialRadius_coordRay_ne_zero_proved partial_sr_holds := partialDeriv_v2_spatialRadius_proved partial_inv_holds := partialDeriv_v2_radialInv_proved diff_at_holds := differentiableAt_coordRay_partialDeriv_v2_radialInv_proved lap_zero_holds := laplacian_radialInv_zero_no_const_provedformal statement (Lean)
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
proof body
Tactic-mode proof.
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-- ... 8 more lines elided ...