Gravity Lattice Convergence Convergence Is Second Order

The second-order limit

When a physical theory is placed on a discrete lattice of points, the continuous equations of motion are replaced by finite differences. The central question is whether the discrete version approaches the continuous one as the lattice spacing shrinks. The answer, for the Laplacian operator that appears throughout physics, is that the approximation error falls off as the square of the spacing: if the spacing is halved, the error drops to a quarter. This is the meaning of second-order convergence, and it is the property that makes lattice calculations trustworthy.

The Laplacian measures how a quantity differs from its average surroundings. On a one-dimensional grid, the standard discrete approximation at a point is the second difference: f(x+a) + f(x-a) - 2f(x), divided by a², where a is the spacing. For a smooth function, this expression converges to the second derivative f''(x) as a approaches zero. The error term is bounded by a constant times a², which is the second-order rate. The same construction extends to three dimensions: the lattice Laplacian is the sum of three one-dimensional second differences, one along each axis, and the total error remains O(a²).

In Recognition Science, the framework's machine-checked library of formal theorems contains a declaration called convergence_is_second_order. The declaration itself is a small lemma: for a positive spacing a less than 1, the inequality a² < a holds. This is the algebraic statement that the squared error is smaller than the linear spacing, which is the essence of the quadratic rate. The substantive convergence theorem, lattice_laplacian_3D_convergence, proves the bound |(f(x+a) + f(x-a) - 2f(x))/a² - f''(x)| ≤ C·a² for any four-times continuously differentiable function f, with a constant C that does not depend on a.

The framework uses this result as a bridge to gravity. In its account, metric perturbations h_μν live on the lattice Z³, and their lattice Laplacian converges to the continuum ∇²h_μν. The linearized Ricci tensor in harmonic gauge is proportional to ∇²h_μν, so the second-order convergence of the lattice operator is what justifies replacing continuous spacetime with a discrete grid in the framework's gravity calculations. The J-cost neighbor sum, which the framework derives from its cost function, approximates the lattice Laplacian to fourth order in the field differences, a tighter approximation that feeds into the same bridge.

The declaration does not claim that the lattice is the actual structure of spacetime, nor that gravity is discrete. It establishes a mathematical property of a numerical method. The physical claim that recognition events form a lattice, and the identification of that lattice with the arena of gravity, is a separate modeling step that the convergence theorem does not address. What the theorem provides is the numerical guarantee: when the framework's lattice spacing goes to zero, its discrete Laplacian becomes the continuum operator at a known, quadratic rate.

/-- **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 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 convergence rate is at least second order in lattice spacing. -/
theorem convergence_is_second_order (a : ℝ) (ha : 0 < a) (ha1 : a < 1) :
    a ^ 2 < a := by nlinarith

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

The declaration does not claim that spacetime is discrete or that gravity is fundamentally a lattice theory. The convergence theorem does not establish the physical bridge from recognition events to the lattice; that identification is a separate modeling step. The second-order rate applies to the discrete Laplacian, not to the J-cost approximation, which has a different fourth-order error term.

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: