Gravity Lattice Convergence Scaled Laplacian Sign

A sign preserved by scaling

The Laplacian is a measure of how a quantity at a point compares with its neighbors: positive where the point is lower than the average of its surroundings, negative where it is higher. On a three-dimensional grid, the lattice Laplacian computes this by adding up second differences along each of the three axes. The scaled lattice Laplacian divides that sum by the square of the grid spacing a, a step that lets a discrete model approach a continuous one as a shrinks toward zero.

In the machine-checked library of formal theorems, the declaration scaled_laplacian_sign proves a modest but useful fact: if the lattice Laplacian is positive at a point, then the scaled version is positive there too, provided the spacing a is nonzero. The proof is a direct application of the fact that dividing a positive number by a positive square preserves its sign. This is not a statement about convergence or about gravity itself; it is a sign-preservation lemma, the kind of small step that larger proofs rely on without pausing to justify.

The declaration sits inside a chain of results about lattice Laplacians. A companion theorem shows the three-dimensional lattice Laplacian is exactly the sum of three one-dimensional second-difference operators, one per axis. Another proves that, for a smooth function sampled on the grid, the scaled lattice Laplacian converges to the continuum Laplacian with error on the order of a squared. The sign lemma does not participate in those convergence arguments directly; it stands apart as a separate, simpler observation.

In Recognition Science, the lattice Laplacian appears as the kinetic operator in a lattice action, and its continuum limit connects to the linearized Ricci tensor for metric perturbations in harmonic gauge. That bridge is a stated intention in the documentation, not a proved theorem in this file. The sign lemma itself makes no claim about physics: it says nothing about the speed of light, the value of Newton's constant, or the behavior of gravitational waves. It merely records that scaling by a positive factor cannot flip the sign of a positive lattice Laplacian.

What the declaration changes for a reader is small but concrete: it certifies one algebraic identity that any larger proof about lattice gravity can invoke without re-deriving it. The convergence theorems carry the weight; the sign lemma is a supporting pillar. A reader who wants to know whether the framework's discrete gravity actually approaches continuum physics should look at the convergence results, not at this sign-preservation fact.

/-- The scaled lattice Laplacian is positive when the lattice Laplacian is positive. -/
theorem scaled_laplacian_sign (f : LatticeField3) (x : Fin 3 → ℤ) (a : ℝ) (ha : a ≠ 0)
    (hf : 0 < lattice_laplacian f x) :
    0 < scaled_lattice_laplacian f x a := by
  unfold scaled_lattice_laplacian
  exact div_pos hf (by positivity)

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

What this page does not claim

The sign lemma does not establish convergence of the lattice Laplacian to the continuum Laplacian. The declaration does not prove that the lattice Laplacian itself is positive for any particular field. The bridge from lattice Laplacian to the linearized Ricci tensor is a documented intention, not a proved theorem in this file.

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: