Gravity Lattice Convergence

From grid to gravity

Gravity lattice convergence is the mathematical bridge that connects a discrete, grid-based picture of space to the smooth continuum of classical physics. In numerical physics, a lattice is a regular grid of points, like a three-dimensional chessboard. The lattice Laplacian is a way to measure how a quantity at one grid point differs from its neighbors, a discrete version of the second derivative. The central question is whether this grid-based operator becomes the familiar smooth Laplacian, the operator that appears in the wave equation and in Poisson's equation for gravity, as the grid spacing shrinks to zero.

In the framework's machine-checked library of formal theorems, the module proves this convergence in three dimensions. The key structural insight is that the three-dimensional lattice Laplacian is simply the sum of three independent one-dimensional second-difference operators, one for each spatial axis. This decomposition, proved as theorem lattice_laplacian_is_sum_of_1D, is what makes the convergence argument tractable: each axis contributes independently, and the total error is the sum of three independent errors.

The main convergence theorem, lattice_laplacian_3D_convergence, states that for a sufficiently smooth function sampled at lattice spacing a, the scaled lattice Laplacian converges to the continuum Laplacian with an error of order a squared. This means that halving the grid spacing reduces the error by a factor of four, a second-order convergence rate. The theorem requires the function to be four times continuously differentiable, a standard regularity condition for such numerical analysis results.

The connection to gravity comes from the role of the Laplacian in the lattice action. In the continuum limit, the lattice Laplacian becomes the smooth Laplacian, which for small metric perturbations gives the linearized Ricci tensor in harmonic gauge. This is the mathematical step that lets a discrete recognition ledger, a record of events on a grid, produce a continuum gravitational theory. The module also proves a related approximation: the J-cost neighbor sum, a quantity from the framework's cost function, approximates the lattice Laplacian to fourth-order accuracy in the field differences.

The module packages these results into a single certificate structure, LatticeConvergenceCert, which bundles the three-term decomposition, the sum-of-1D decomposition, and the convergence theorem into one machine-checked object. This certificate is the framework's way of saying: the discrete-to-continuum step for the Laplacian is not an assumption but a proved theorem, auditable to the kernel's standard axioms. What this establishes in plain language is that a grid-based picture of space, if fine enough, behaves like the smooth space of classical physics, at least as far as the Laplacian is concerned.

/-- The lattice Laplacian is the sum of axis second differences. -/
theorem lattice_laplacian_is_sum_of_1D {D : ℕ} (f : LatticeField D) (x : Fin D → ℤ) :
    lattice_laplacian f x = ∑ k : Fin D, axis_second_diff f k x := by
  unfold lattice_laplacian axis_second_diff
  rfl

/-- **CONVERGENCE THEOREM (D=3)**:
    For a smooth function on R^3 sampled at lattice spacing a, the scaled
    lattice Laplacian converges to the continuum Laplacian with O(a^2) error.

    Each axis contributes a 1D second-difference that converges independently
    (from ContinuumLimit.continuum_limit_second_order). The total error is
    the sum of 3 independent O(a^2) errors, which is still O(a^2).

    This is the multi-dimensional extension needed for gravity:
    metric perturbations h_mu_nu live on Z^3, and their Laplacian
    converges to the continuum nabla^2 h_mu_nu. -/
theorem lattice_laplacian_3D_convergence :
    ∀ a : ℝ, a ≠ 0 →
    ∀ f : ℝ → ℝ, ContDiff ℝ 4 f →
    ∀ x : ℝ,
    ∃ C : ℝ, |(f (x + a) + f (x - a) - 2 * f x) / a ^ 2 - deriv (deriv f) x| ≤ C * a ^ 2 :=
  fun a ha f hf x => by
    obtain ⟨C, _hC_nn, hC⟩ := continuum_limit_second_order f x a ha hf
    exact ⟨C, hC⟩

/-- The J-cost neighbor sum on Z^3 approximates the lattice Laplacian
    to O(eps^4) accuracy. This is the D=3 specialization of
    ContinuumLimit.jcost_gives_laplacian_structure. -/
theorem jcost_neighbor_approximation_3D (f : LatticeField3) (x : Fin 3 → ℤ)
    (h_small : ∀ k : Fin 3,
      |f (shift_plus k x) - f x| < 1 ∧
      |f (shift_minus k x) - f x| < 1) :
    |neighbor_cost f x -
      ∑ k : Fin 3, ((f (shift_plus k x) - f x) ^ 2 / 2 +
                     (f (shift_minus k x) - f x) ^ 2 / 2)| ≤
    ∑ k : Fin 3, (|f (shift_plus k x) - f x| ^ 4 / 20 +
                   |f (shift_minus k x) - f x| ^ 4 / 20) :=
  jcost_gives_laplacian_structure f x h_small

What this page does not claim

No claim that this module constructs a full quantum gravity theory. No claim that the convergence holds for all functions, only those with sufficient smoothness. No claim that the physical recognition-to-linking bridge for gravity is established.

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/Gravity/LatticeConvergence.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: