Gravity Regge Cubic Lattice Limit Finite Difference Second Order Estimate

The lattice estimate

In numerical analysis, the standard way to approximate the second derivative of a function f at a point x uses values at x-a and x+a: the expression (f(x+a) + f(x-a) - 2f(x)) / a². This is the central difference quotient. For a smooth function, this quotient approaches the true second derivative as the step size a shrinks to zero. The classical question is how fast it converges.

The Recognition Science framework's machine-checked library of formal theorems contains a precise answer, the declaration finite_difference_second_order_estimate. It proves that if the function is four times continuously differentiable, then the absolute difference between this finite difference quotient and the true second derivative is bounded by some constant times a². In other words, the error shrinks quadratically with the step size. Halving the step cuts the error by a factor of four, in the worst case. This is a standard result in numerical analysis, but here it is verified by a computer-checked proof, meaning no step in the reasoning is left to human judgment.

The theorem is not a statement about a specific function or a specific lattice. It is a universal statement: for any sufficiently smooth real-valued function, for any point, and for any nonzero step size, the quadratic error bound holds. The proof is constructive in the sense that it guarantees the existence of the error constant, but it does not compute its value. The constant depends on the function's behavior, specifically on its fourth derivative.

This estimate serves as the analytic ingredient in a larger framework project: showing that a discrete version of gravity, built on a cubic lattice of tetrahedra, converges to the continuum theory as the lattice spacing goes to zero. The finite difference result provides the local error control needed for that global convergence argument. The framework's library uses this theorem as a component in the proof that the second-order Regge action, a discrete approximation to Einstein's equations, has the correct continuum limit on a regular cubic lattice.

What the theorem does not claim is just as important. It does not prove that any particular lattice model of gravity converges. It only establishes the local error bound for the finite difference approximation of a single function's second derivative. The connection from this local estimate to a full theory of quantum gravity, including the physical interpretation of the lattice as spacetime, is a separate and much larger step. The framework's library is explicit that the physical bridge from the discrete action to the continuum is an open target, not a proved theorem.

/-- The existing one-dimensional finite-difference theorem is the analytic
ingredient used in the cubic-lattice model. -/
theorem finite_difference_second_order_estimate
    (f : ℝ → ℝ) (x a : ℝ) (ha : a ≠ 0) (hf : ContDiff ℝ 4 f) :
    ∃ C : ℝ, 0 ≤ C ∧
      |(f (x + a) + f (x - a) - 2 * f x) / a ^ 2 -
        deriv (deriv f) x| ≤ C * a ^ 2 :=
  CubicReggeConvergence.weak_field_error_estimate f x a ha hf

What this page does not claim

This does not prove that any specific lattice model of gravity converges to the continuum. This does not provide a numerical value for the error constant C. This does not establish the physical interpretation of the lattice as spacetime.

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