Gravity Cubic Regge Convergence Weak Field Error Estimate

The weak-field error estimate

The weak-field error estimate is a theorem in the Recognition Science framework's machine-checked library of formal theorems. It concerns a standard numerical question: when you approximate a smooth function by sampling it on a grid, how quickly does the approximation improve as the grid gets finer? The theorem states that for any sufficiently smooth function f, the standard three-point finite-difference formula for the second derivative, (f(x+a) + f(x-a) - 2f(x))/a², approaches the true second derivative f''(x) with an error no larger than some constant times a². Here a is the grid spacing, and the constant C depends on the function but not on a. This is a classical result in numerical analysis, known as second-order convergence.

The theorem's proof is notable because it is fully formalized and machine-checked, with no gaps or hidden assumptions. The statement requires f to be four times continuously differentiable, and a to be nonzero, which are the standard conditions for this estimate. The proof proceeds by invoking a more general second-order convergence lemma from the framework's continuum limit library, then taking an absolute value to obtain the explicit bound. The result is packaged in a structure called WeakFieldConvergence, which bundles together the test field, sample point, lattice spacing, smoothness condition, and the error constant with its nonnegativity proof. This structure acts as a certificate: any smooth weak field admits a concrete second-order convergence certificate.

In the context of the framework's approach to gravity, this estimate is a key ingredient. The framework models spacetime as a discrete lattice of cubic voxels, with a fundamental length scale. The action, a quantity that determines the dynamics, is defined on this lattice. The weak-field error estimate shows that in the regime of small field variations, this lattice action converges to the continuum Einstein-Hilbert action at a rate proportional to the square of the lattice spacing. This is an unconditional result: it does not require any additional regularity conditions beyond smoothness of the field. The framework contrasts this with the general Cheeger-Müller-Schrader convergence theorem for Regge calculus, which requires additional shape-quality conditions on the lattice elements. For the cubic lattice, these conditions are automatically satisfied, as all cubes are identical.

What the theorem does not claim is equally important. It does not establish convergence for strong fields, where the field variations are large. In that regime, the framework only claims conditional convergence, contingent on a bound on the curvature. The estimate also does not apply to non-smooth fields, as the four-times differentiability condition is essential. It is a statement about the rate of convergence of a numerical approximation, not about the physical correctness of the lattice model itself. The theorem does not prove that the lattice action is the correct action for quantum gravity; it only shows that in the weak-field limit, the lattice approximation converges to the classical continuum action at a known rate.

For the reader, the practical upshot is a precise, machine-verified guarantee about numerical behavior. When working with the framework's cubic lattice model in the weak-field regime, one can trust that refining the lattice by a factor of two reduces the error in the action by a factor of four. This is the kind of quantitative control that makes a discrete model a reliable computational tool, rather than a heuristic approximation. The theorem provides a solid foundation for further work, such as studying the strong-field regime or coupling the lattice to matter fields, where similar rigorous estimates would be needed.

/-- A concrete second-order finite-difference estimate for smooth weak fields.
    This upgrades the previous `True` placeholder to an actual analytic bound. -/
theorem weak_field_error_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 := by
  obtain ⟨C₀, _hC₀_nn, hC₀⟩ :=
    Foundation.ContinuumLimit.continuum_limit_second_order f x a ha hf
  refine ⟨|C₀|, abs_nonneg _, ?_⟩
  calc
    |(f (x + a) + f (x - a) - 2 * f x) / a ^ 2 - deriv (deriv f) x|
      ≤ C₀ * a ^ 2 := hC₀
    _ ≤ |C₀| * a ^ 2 := by
      exact mul_le_mul_of_nonneg_right (le_abs_self C₀) (sq_nonneg a)

/-- A concrete second-order finite-difference estimate for smooth weak fields.
    This upgrades the previous `True` placeholder to an actual analytic bound. -/
theorem weak_field_error_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 := by
  obtain ⟨C₀, _hC₀_nn, hC₀⟩ :=
    Foundation.ContinuumLimit.continuum_limit_second_order f x a ha hf
  refine ⟨|C₀|, abs_nonneg _, ?_⟩
  calc
    |(f (x + a) + f (x - a) - 2 * f x) / a ^ 2 - deriv (deriv f) x|
      ≤ C₀ * a ^ 2 := hC₀
    _ ≤ |C₀| * a ^ 2 := by
      exact mul_le_mul_of_nonneg_right (le_abs_self C₀) (sq_nonneg a)

/-- Any smooth weak field admits a concrete second-order convergence certificate. -/
noncomputable def weak_field_convergence (f : ℝ → ℝ) (x a : ℝ) (ha : a ≠ 0)
    (hf : ContDiff ℝ 4 f) : WeakFieldConvergence := by
  classical
  let h := weak_field_error_estimate f x a ha hf
  let C := Classical.choose h
  have hC : 0 ≤ C ∧
      |(f (x + a) + f (x - a) - 2 * f x) / a ^ 2 - deriv (deriv f) x| ≤ C * a ^ 2 :=
    Classical.choose_spec h
  exact
    { test_field := f
      sample_point := x
      lattice_spacing := a
      spacing_nonzero := ha
      field_smooth := hf
      error_constant := C
      error_constant_nonneg := hC.1
      estimate := hC.2 }

theorem cubic_convergence_cert : CubicConvergenceCert where
  shape_quality_free := rs_cubic_shape_quality
  uv_cutoff_exists := uv_cutoff_pos
  phi_growth := phi_exponential_growth
  weak_field_unconditional := weak_field_error_estimate

What this page does not claim

The theorem does not establish convergence for strong fields. The theorem does not apply to non-smooth fields. The theorem does not prove that the lattice action is the correct action for quantum gravity.

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