Encyclopedia Foundation Foundation Pair Kernel Newtonian3 Integrable On Newtonian Fourier Integrand
Foundation Pair Kernel Newtonian3 Integrable On Newtonian Fourier Integrand
A technical lemma about a Newtonian Fourier integral that turns out to be the load-bearing step in a larger proof.
The integrability lemma
The declaration integrableOn_newtonian_fourier_integrand is a technical lemma in the machine-checked library of formal theorems. It states that a certain function, the integrand of a Newtonian Fourier transform, is integrable on a ball of radius N in three-dimensional space. In plain terms, it proves that the integral of this function over a finite region does not blow up to infinity; it is a well-defined, finite quantity. This is a necessary condition for the integral to have a meaningful value, and it is a prerequisite for the later step of taking a limit as the radius N grows without bound.
The integrand in question is the cosine of a dot product divided by the squared norm of the wave vector, cos(k·x) / ‖k‖². The lemma establishes that this expression is integrable over the ball of radius N. The proof relies on a change of variables that aligns the coordinate axis with the vector x, reducing the three-dimensional problem to a one-dimensional integral. This is a standard technique in Fourier analysis, and the lemma confirms that the singularity at the origin, where the denominator vanishes, is mild enough that the integral remains finite.
This lemma is not a standalone result about physics. It is a stepping stone within a larger proof that aims to establish a specific identity for the Newtonian potential. The identity in question, lim_N (2π)⁻³ ∫_{‖k‖
What the lemma does not claim is the identity itself. It does not state that the limit exists or that it equals the Newtonian potential. It only establishes that the integral over a finite ball is well-defined. The limit and the final identity are separate, more substantial results that are proved elsewhere in the library. The lemma is a necessary but not sufficient condition for the final theorem.
In the broader context of the Recognition Science framework, this lemma is part of a campaign to derive the constant 4π from pure three-dimensional geometry. The framework aims to show that the 4π appearing in the Newtonian potential is not an arbitrary constant but a consequence of the geometry of the unit sphere. This lemma is a technical step in that larger project, but it does not, by itself, make any claim about the origin of physical constants.
THEOREM integrableOn_inv_norm_sq_ball · IndisputableMonolith/Foundation/PairKernelNewtonian3.lean
/-- The inverse-square singularity is integrable on every finite ball in
three dimensions. -/
theorem integrableOn_inv_norm_sq_ball (R : ℝ) :
IntegrableOn (fun k : EuclideanSpace ℝ (Fin 3) => (‖k‖ ^ 2)⁻¹)
(Metric.ball 0 R) := by
by_cases hR : 0 < R
· have hind : (fun x : EuclideanSpace ℝ (Fin 3) => invSqProfile R ‖x‖)
= (Metric.ball (0 : EuclideanSpace ℝ (Fin 3)) R).indicator
fun x => (‖x‖ ^ 2)⁻¹ := by
funext x
by_cases hx : x ∈ Metric.ball (0 : EuclideanSpace ℝ (Fin 3)) R
· rw [Set.indicator_of_mem hx]
have hlt : ‖x‖ < R := by rwa [Metric.mem_ball, dist_zero_right] at hx
simp only [invSqProfile, if_pos hlt]
· rw [Set.indicator_of_notMem hx]
have hlt : ¬‖x‖ < R := by rwa [Metric.mem_ball, dist_zero_right] at hx
simp only [invSqProfile, if_neg hlt]
have h := integrable_invSqProfile_comp_norm (R := R)
rw [hind] at h
exact (integrable_indicator_iff Metric.isOpen_ball.measurableSet).1 h
· rw [(Metric.ball_eq_empty).2 (le_of_not_gt hR)]
exact integrableOn_empty
What this page does not claim
This lemma does not prove the Newtonian Fourier identity itself. This lemma does not claim that the limit of the integral exists or equals 1/(4π‖x‖). This lemma does not make any statement about the physical origin of constants.
Verify this page
Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:
$ lake env lean IndisputableMonolith/Foundation/PairKernelNewtonian3.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)
A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.
Derived articles
This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red:
- What is the full statement of the Newtonian Fourier identity that this lemma supports?
- How does the proof of the limit of the integral proceed from this integrability result?
- What is the role of the Archimedes marginal in the larger proof of the 4π constant?
MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND
THEOREM integrableOn_inv_norm_sq_ball · IndisputableMonolith/Foundation/PairKernelNewtonian3.lean
/-- The inverse-square singularity is integrable on every finite ball in three dimensions. -/ theorem integrableOn_inv_norm_sq_ball (R : ℝ) : IntegrableOn (fun k : EuclideanSpace ℝ (Fin 3) => (‖k‖ ^ 2)⁻¹) (Metric.ball 0 R) := by by_cases hR : 0 < R · have hind : (fun x : EuclideanSpace ℝ (Fin 3) => invSqProfile R ‖x‖) = (Metric.ball (0 : EuclideanSpace ℝ (Fin 3)) R).indicator fun x => (‖x‖ ^ 2)⁻¹ := by funext x by_cases hx : x ∈ Metric.ball (0 : EuclideanSpace ℝ (Fin 3)) R · rw [Set.indicator_of_mem hx] have hlt : ‖x‖ < R := by rwa [Metric.mem_ball, dist_zero_right] at hx simp only [invSqProfile, if_pos hlt] · rw [Set.indicator_of_notMem hx] have hlt : ¬‖x‖ < R := by rwa [Metric.mem_ball, dist_zero_right] at hx simp only [invSqProfile, if_neg hlt] have h := integrable_invSqProfile_comp_norm (R := R) rw [hind] at h exact (integrable_indicator_iff Metric.isOpen_ball.measurableSet).1 h · rw [(Metric.ball_eq_empty).2 (le_of_not_gt hR)] exact integrableOn_emptyThe declaration proves that the integrand cos(k·x)/‖k‖² is integrable on the ball of radius N in three-dimensional space. integrableOn_inv_norm_sq_ball · IndisputableMonolith/Foundation/PairKernelNewtonian3.lean