Gravity Lattice Convergence Lattice Convergence Cert

The convergence certificate

The Laplacian is a central operator in physics, measuring how a quantity at a point differs from its average over nearby points. The Recognition Science framework builds its models on a discrete ledger, a record of events on a lattice of points, and needs a version of the Laplacian that works on such a lattice. The declaration lattice_convergence_cert is a machine-checked certificate, a formal proof, that this discrete version behaves correctly: as the lattice spacing shrinks to zero, the lattice Laplacian converges to the smooth continuum Laplacian with an error that shrinks quadratically.

The certificate packages three separate theorems. First, it proves that the three-dimensional lattice Laplacian is exactly the sum of three one-dimensional second-difference operators, one along each axis. Second, it proves that this lattice Laplacian can be decomposed into these axis-wise contributions. Third, and most importantly, it proves the convergence theorem: for any sufficiently smooth function sampled on the lattice, the scaled lattice Laplacian (divided by the square of the spacing) approaches the true Laplacian, with the error bounded by a constant times the square of the spacing. This is the standard second-order accuracy expected of such a finite-difference scheme.

In the framework's account of gravity, this certificate is a load-bearing step. The lattice Laplacian serves as the kinetic operator in the lattice action, and its convergence to the continuum Laplacian is what allows metric perturbations, the small ripples in the geometry, to be described by the smooth equations of general relativity in the limit of zero spacing. The certificate thus bridges the discrete ledger world and the smooth continuum of classical physics.

The certificate is precise about what it does not claim. It does not claim that the lattice Laplacian itself equals the continuum Laplacian, only that it converges to it in the limit. It does not claim to have derived the full Einstein field equations, nor does it claim that the physical universe is actually a lattice. It establishes a mathematical convergence property, not a physical fact about the nature of space. The bridge from the recognition cost function to the lattice Laplacian, the step that connects the framework's foundational cost to this discrete operator, is itself a separate result, not part of this certificate.

theorem lattice_convergence_cert : LatticeConvergenceCert where
  three_terms := D3_laplacian_three_terms
  decomposition := lattice_laplacian_is_sum_of_1D
  convergence := lattice_laplacian_3D_convergence

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

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

What this page does not claim

The certificate does not prove that the physical universe is a lattice. The certificate does not derive the full Einstein field equations, only the convergence of a discrete operator. The certificate does not establish the bridge from the J-cost function to 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: