Gravity Cubic Regge Proof Linearized El Plus Laplacian Zero

The linearized equation

The Laplacian is a central object in physics and mathematics. It measures the difference between a value at a point and the average of its immediate neighbors. In three dimensions, the Laplacian of a function f is often written as ∇²f. It appears in the heat equation, the wave equation, and the Poisson equation for gravity. This declaration concerns a discrete version of that operator, defined on a cubic lattice, and its connection to a specific variational principle.

In the framework of Recognition Science, gravity is derived from a cost function, a measure of the price of recognition events. The variational principle states that nature minimizes the total cost. The Euler-Lagrange equation is the condition for this minimum. For the cost function used here, this equation is nonlinear, involving the hyperbolic sine function. The declaration linearized_el_plus_laplacian_zero proves a key fact about the linearized version of this equation: the linearized Euler-Lagrange expression plus the lattice Laplacian is identically zero. In other words, the linearized equation is exactly the lattice Laplacian equals zero.

This is a purely algebraic identity, proved in the machine-checked library of formal theorems. It holds for any function on a lattice of any dimension D. The proof unfolds the definitions and simplifies the sums. The significance is that it links the nonlinear, cost-based gravity theory to the standard linear operator of classical physics. This is the step that allows the full convergence proof: as the lattice spacing goes to zero, the discrete theory's equations approach the continuum equations of linearized general relativity.

It is important to state what this declaration does not claim. It does not prove that the full nonlinear Euler-Lagrange equation is equal to the Laplacian. It only concerns the linearized version. It does not establish the convergence of the discrete theory to the continuum; that is a separate, more involved theorem. Finally, it does not claim that the lattice Laplacian itself is the true continuum Laplacian; the convergence of the lattice operator to the continuum one is a separate result, requiring smoothness conditions.

/-- **Core algebraic identity**: the linearized EL operator (replacing
    sinh(ε) → ε) sums to minus the lattice Laplacian.

    Σₖ [(f(x) − f(x−eₖ)) − (f(x+eₖ) − f(x))]
    = Σₖ [2f(x) − f(x+eₖ) − f(x−eₖ)]
    = −Σₖ [f(x+eₖ) + f(x−eₖ) − 2f(x)]
    = −lattice_laplacian(f)(x) -/
theorem linearized_el_plus_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))) +
    lattice_laplacian f x = 0 := by
  unfold lattice_laplacian
  rw [← Finset.sum_add_distrib]
  apply Finset.sum_eq_zero
  intro k _; ring

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

What this page does not claim

This declaration does not prove that the full nonlinear Euler-Lagrange equation equals the Laplacian. This declaration does not establish convergence of the discrete theory to the continuum. This declaration does not claim the lattice Laplacian is identical to the continuum Laplacian without additional smoothness conditions.

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: