Gravity Cubic Regge Proof Linearized El Eq Neg Laplacian

The linearized equation

The Laplacian is a standard measure of how a quantity at one point differs from its neighbors. For a smooth function on ordinary space, it is the sum of the second derivatives in each direction. On a discrete lattice, the natural analogue compares a value at a site with the values at its immediate neighbors. The declaration in question proves a precise identity for this discrete setting.

The framework's cost, a forced price for each recognition event, has a specific form whose derivative is the hyperbolic sine. When the field values are nearly constant, the sine can be replaced by its linear approximation. The theorem linearized_el_eq_neg_laplacian states that this linearized Euler-Lagrange expression is exactly the negative of the lattice Laplacian. In symbols, the sum over all directions of the difference between the value at a site and its neighbors equals minus the lattice Laplacian at that site.

This is a purely algebraic identity on the lattice, proved by rearranging sums. It does not involve limits or calculus. A companion result shows that the linearized equation is zero if and only if the lattice Laplacian is zero. That equivalence is what connects the framework's variational principle to the standard discrete Laplace equation.

The theorem is one step in a longer convergence argument. The framework's library of machine-checked theorems also proves that the full nonlinear cost action approaches the quadratic action as the lattice spacing shrinks, and that the lattice Laplacian divided by the spacing squared approaches the continuum Laplacian. The linearization identity is the bridge between those two limits. It shows that the Euler-Lagrange equations of the framework's cost, in the small-field regime, are the discrete Laplace equation.

What the declaration does not claim is any statement about the continuum limit itself. It does not assert that solutions of the linearized lattice equation converge to solutions of the continuum Laplace equation. It does not claim that the full nonlinear equation behaves like the linear one away from small fields. It does not identify the lattice Laplacian with any particular physical operator beyond the algebraic definition on the lattice. The theorem is a discrete identity, and its role in the convergence proof is to show that the linearized variational principle has the right structure.

/-- The linearized EL equation equals minus the lattice Laplacian. -/
theorem linearized_el_eq_neg_laplacian {D : ℕ}
    (f : LatticeField D) (x : Fin D → ℤ) :
    (∑ k : Fin D,
      ((f x - f (shift_minus k x)) -
       (f (shift_plus k x) - f x))) =
    -lattice_laplacian f x := by
  linarith [linearized_el_plus_laplacian_zero f x]

/-- The linearized EL equation δS/δf = 0 is equivalent to the
    lattice Laplace equation: Δ_lat f = 0. -/
theorem linearized_el_zero_iff_laplacian_zero {D : ℕ}
    (f : LatticeField D) (x : Fin D → ℤ) :
    (∑ k : Fin D,
      ((f x - f (shift_minus k x)) -
       (f (shift_plus k x) - f x))) = 0 ↔
    lattice_laplacian f x = 0 := by
  rw [linearized_el_eq_neg_laplacian]
  constructor <;> intro h <;> linarith

/-- The total J-cost on the lattice approximates the quadratic action.
    For D-dimensional lattice with small perturbations:

    |Σ_{x,k} J_log(εₖ(x)) − Σ_{x,k} εₖ(x)²/2|
    ≤ Σ_{x,k} |εₖ(x)|⁴/20

    This is `jcost_gives_laplacian_structure` from ContinuumLimit. -/
theorem total_action_convergence {D : ℕ}
    (f : LatticeField D) (x : Fin D → ℤ)
    (h_small : ∀ k : Fin D,
      |f (shift_plus k x) - f x| < 1 ∧
      |f (shift_minus k x) - f x| < 1) :
    |neighbor_cost f x -
      ∑ k : Fin D, ((f (shift_plus k x) - f x) ^ 2 / 2 +
                     (f (shift_minus k x) - f x) ^ 2 / 2)| ≤
    ∑ k : Fin D, (|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

/-- The lattice Laplacian (scaled by 1/a²) converges to the continuous
    Laplacian ∇² at O(a²). This is the standard finite-difference result,
    already proved in ContinuumLimit.lean. -/
theorem laplacian_continuum_limit (f : ℝ → ℝ) (x a : ℝ)
    (ha : a ≠ 0) (hf : ContDiff ℝ 4 f) :
    ∃ C : ℝ,
      |(f (x + a) + f (x - a) - 2 * f x) / a ^ 2 -
        deriv (deriv f) x| ≤ C * a ^ 2 := 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 theorem does not assert convergence of solutions of the linearized lattice equation to continuum solutions. The theorem does not claim the linearized equation approximates the nonlinear one for large field differences. The theorem does not identify the lattice Laplacian with a physical operator beyond its algebraic definition.

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/CubicReggeProof.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: