Foundation Pair Kernel Newtonian3

The 4π of three dimensions

The number 4π is the surface area of a unit sphere. For a sphere of radius 1 in three-dimensional space, the area of its surface is exactly 4π. This is a classical fact of geometry, known since Archimedes, and it is the starting point for a module in the Recognition Science framework's machine-checked library of formal theorems. The module, called foundation pair kernel newtonian3, proves that the famous 1/r form of the Newtonian potential, the force law that governs gravity and electrostatics, is not an arbitrary choice but a necessary consequence of living in three dimensions.

The proof works by translating the problem into Fourier space, where the potential's behavior is encoded in the geometry of the sphere. The key identity, proved as a theorem, is that three times the volume of the unit ball in ℝ³ equals 4π. This single fact, the surface area of the unit sphere, is the geometric origin of the constant that appears in the Newtonian potential. The module proves this identity in two ways: once through the ball's volume, and once directly from the surface measure of the sphere. Both routes arrive at the same 4π.

The central result is the Newtonian Fourier identity: the limit as N grows of (2π)⁻³ times the integral over a ball of radius N of cos(k·x)/‖k‖² dk equals 1/(4π‖x‖). This is a precise statement that the inverse-square law, with its 1/r dependence, is the Fourier transform of the 1/‖k‖² kernel in three dimensions. The proof uses rotation invariance to reduce any separation vector to the first coordinate axis, then evaluates the integral through a series of one-dimensional steps, including the Dirichlet integral ∫₀^∞ sin(t)/t dt = π/2.

The module deliberately imports no lattice or recognition machinery. Its job is to pin down the geometric origin of 4π independently, so that later stages of the framework can build on this pure geometric fact. One geometric bridge remains unproved: the claim that the first coordinate of the unit-sphere measure has density 2π on the interval [-1,1]. This is stated but not proved, and it is a target for future work. The module also states, but does not prove, the full Newtonian Fourier identity as a separate target.

What this establishes in plain language is that the 1/r law is not a mystery. In three dimensions, the geometry of the sphere forces the potential to fall off as the inverse of distance. The framework's library shows this with machine-checked rigor, and the proof is a pure fact of three-dimensional geometry, independent of any physical assumptions about gravity or recognition.

/-- The ambient three-dimensional Euclidean carrier for the Newtonian angular
leaf. -/
abbrev E3 : Type := EuclideanSpace ℝ (Fin 3)

/-- The surface measure on the unit sphere in `ℝ³`, as obtained from Lebesgue
measure by Mathlib's generalized polar-coordinate construction. -/
abbrev sphereMeasure3 : Measure S2 := (volume : Measure E3).toSphere

theorem newtonian_fourier_target : NewtonianFourierTarget := by
  intro x hx
  have ha : 0 < ‖x‖ := norm_pos_iff.2 hx
  have hscale :
      Filter.Tendsto (fun N : ℝ => ‖x‖ * N) Filter.atTop Filter.atTop :=
    Filter.tendsto_atTop.2 fun b => by
      filter_upwards [Filter.eventually_ge_atTop (b / ‖x‖)] with N hN
      have h := (div_le_iff₀ ha).1 hN
      simpa [mul_comm] using h
  have hdir :=
    dirichlet_sine_integral_tendsto.comp hscale
  have haxis :
      Filter.Tendsto
        (fun N : ℝ =>
          ∫ k in Metric.ball (0 : E3) N,
            Real.cos (‖x‖ * k 0) / ‖k‖ ^ 2)
        Filter.atTop
        (nhds ((4 * Real.pi / ‖x‖) * (Real.pi / 2))) := by
    apply (hdir.const_mul (4 * Real.pi / ‖x‖)).congr'
    filter_upwards [Filter.eventually_gt_atTop (0 : ℝ)] with N hN
    exact (axis_ball_integral_formula ‖x‖ N ha hN).symm
  have horiginal :
      Filter.Tendsto
        (fun N : ℝ =>
          ∫ k in Metric.ball (0 : E3) N,
            Real.cos (∑ i, k i * x i) / ‖k‖ ^ 2)
        Filter.atTop
        (nhds ((4 * Real.pi / ‖x‖) * (Real.pi / 2))) := by
    apply haxis.congr'
    exact Filter.Eventually.of_forall fun N =>
      (newtonian_integral_rotate_to_axis x N).symm
  have hnormalized :=
    horiginal.const_mul (1 / (2 * Real.pi) ^ 3)
  convert hnormalized using 1
  field_simp [Real.pi_ne_zero, ha.ne']
  ring_nf

What this page does not claim

The module does not prove the full Newtonian Fourier identity as a standalone target; it is stated but not proved here. The module does not derive any physical force law or connect 4π to gravity or recognition. The module does not prove the Archimedes marginal density claim; it remains an open geometric bridge.

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: