Gravity Cubic Regge Proof Linearized El Zero Iff Laplacian Zero

The linearized equation

The declaration linearized_el_zero_iff_laplacian_zero is a theorem in the framework's machine-checked library of formal theorems. It states a precise equivalence for a field defined on a cubic lattice: the linearized Euler-Lagrange equation of the framework's cost function is zero at a point if and only if the lattice Laplacian of the field is zero at that point. In plain words, the condition that a small perturbation feels no restoring force is exactly the condition that the field is harmonic, meaning its value at a point equals the average of its neighbors.

The proof is a short algebraic identity. The linearized Euler-Lagrange expression is shown to be the negative of the lattice Laplacian, and a number is zero exactly when its negative is zero. The theorem holds in any dimension D, for any lattice field, at any lattice point. It is a statement about the discrete structure itself, not about the continuum limit.

This equivalence is a stepping stone in a larger proof that the framework's discrete gravity action converges to the continuum Einstein field equations in the limit of a fine lattice. The linearization step is what connects the discrete equations of motion to the familiar Laplacian of continuum physics. The theorem does not claim that the full nonlinear Euler-Lagrange equation is equivalent to the Laplacian; it applies only to the linearized version. It also does not claim that a harmonic field on the lattice is the same as a solution to the full discrete equations of motion, only that the linearized condition matches the Laplacian condition.

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

The theorem does not claim that the full nonlinear Euler-Lagrange equation is equivalent to the Laplacian. It does not claim that a harmonic field on the lattice is a solution to the full discrete equations of motion. It does not claim anything about the continuum limit or the physical interpretation of the lattice field.

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: