Gravity Lattice Convergence Lattice Laplacian Is Sum Of 1 D

The lattice Laplacian

The Laplacian is a standard tool that measures how a quantity at a point differs from its neighbors. On a continuous space, it is the sum of second derivatives along each axis. On a discrete grid, the same idea becomes a finite difference: take the value at a point, subtract twice the value at its center, and add the values at its two neighbors along a given axis. For a grid in three dimensions, the discrete Laplacian is simply the sum of these one-dimensional second differences along the x, y, and z axes. This decomposition, proved in the framework's machine-checked library of formal theorems, is the declaration lattice_laplacian_is_sum_of_1D.

The proof is a direct computation. The definition of the lattice Laplacian sums the second difference over all three axes, and the theorem verifies that this sum equals the sum of the individual axis second differences. The result holds for any dimension D, not just three, and for any grid point. The three-dimensional case is then a specialization: the sum has exactly three terms, one for each axis. This is not a physical assumption but a mathematical identity that follows from the definitions.

The importance for gravity is that the lattice Laplacian is the kinetic operator in a lattice action. In the continuum limit, as the grid spacing a approaches zero, the scaled lattice Laplacian converges to the continuum Laplacian ∇² with an error of order a². The framework proves this convergence for smooth functions on R³. The decomposition into independent axes is what makes the convergence work: each axis contributes a one-dimensional second difference that converges independently, and the total error is the sum of three independent order-a² errors, which is still order a².

In Recognition Science, this convergence is a bridge from the discrete ledger of recognition events to the smooth equations of gravity. The framework models metric perturbations h_μν as living on the lattice Z³, and their lattice Laplacian converges to the continuum ∇² h_μν, which appears in the linearized Ricci tensor in harmonic gauge. The theorem establishes the mathematical identity and the convergence rate. It does not claim that the physical bridge from recognition to linking is complete; that remains an open target. It also does not claim that the lattice itself is the true structure of spacetime, only that the discrete operator converges to the continuum one in the appropriate limit.

/-- 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

/-- The lattice Laplacian on Z^3 is the sum of 3 second-difference operators. -/
theorem D3_laplacian_three_terms (f : LatticeField3) (x : Fin 3 → ℤ) :
    lattice_laplacian f x =
      (f (shift_plus 0 x) + f (shift_minus 0 x) - 2 * f x) +
      (f (shift_plus 1 x) + f (shift_minus 1 x) - 2 * f x) +
      (f (shift_plus 2 x) + f (shift_minus 2 x) - 2 * f x) := by
  unfold lattice_laplacian
  simp [Fin.sum_univ_three]
  ring

/-- **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⟩

What this page does not claim

The physical bridge from recognition to linking is complete. The lattice is the true structure of spacetime. The convergence theorem applies to non-smooth fields. The framework derives the full Einstein equations from the lattice Laplacian.

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: