Gravity Cubic Regge Convergence Rscubic Convergence Conditions

Convergence conditions on a cubic lattice

Regge calculus is a way of doing general relativity on a discrete grid: instead of smooth spacetime, you have a lattice of flat pieces, and curvature lives on the hinges where the pieces meet. A central question is whether the discrete theory approaches the continuous one as the grid gets finer. The classical answer, due to Cheeger, Müller, and Schrader, gives three conditions under which convergence is guaranteed: a bound on the curvature, a bound on the quality of the lattice cells (how far they are from being regular), and a bound on the mesh size relative to the curvature scale.

In the Recognition Science framework, the relevant lattice is the cubic lattice Z³, and the declaration RSCubicConvergenceConditions packages the conditions needed for convergence in that specific setting. The key simplification is that on a perfect cubic lattice, the shape quality is exactly 1: every cell is a perfect cube, so the aspect-ratio condition of the general theorem is automatically satisfied. The declaration therefore records only two substantive requirements: a positive curvature bound K, and a mesh threshold of 1/K below which the lattice spacing must fall. This is the same mesh condition as in the general theory; the shape condition is the one that becomes free.

The declaration is part of a larger machine-checked library of formal theorems. The library proves that the shape quality of the cubic lattice is exactly 1, that the weak-field error between the lattice action and the continuum action is bounded by a constant times a², and that the lattice has a natural ultraviolet cutoff coming from its 8-tick periodicity. These results are assembled into a certificate that records the three structural advantages of the cubic lattice: free shape quality, a physical UV cutoff, and exponential growth of resolution with refinement level.

What the declaration does not claim is important. It does not prove that the full Regge convergence theorem holds on the cubic lattice without any conditions; the curvature bound and mesh threshold remain. It does not establish convergence in the strong-field regime without an additional bounded-curvature assumption. And it does not claim that the cubic lattice is the only lattice on which convergence holds, or that the framework's approach supersedes the classical CMS theorem. The declaration is a precise statement of which conditions are needed in a special case, not a claim that the general problem has vanished.

For a reader, the practical upshot is this: on a perfect cubic lattice, one of the three classical conditions is automatically satisfied, leaving two conditions to check. That is a genuine simplification, and it is now a machine-checked fact rather than a heuristic expectation.

/-- For the RS cubic lattice, the CMS conditions simplify:
    (C1) Curvature bound: ||Riem|| < K (still required)
    (C2) Shape quality: σ = 1 (automatically satisfied for cubes)
    (C3) Mesh threshold: a < a₀(K) = 1/K (standard)

    Condition (C2) is FREE for the RS lattice. This removes one
    of the three CMS conditions. -/
structure RSCubicConvergenceConditions where
  K_curvature : ℝ
  K_pos : 0 < K_curvature
  mesh_threshold : ℝ := 1 / K_curvature
  threshold_pos : 0 < mesh_threshold := by positivity

/-- The RS cubic lattice has unit shape quality. -/
theorem rs_cubic_shape_quality : cubic_shape_bound = 1 := rfl

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

What this page does not claim

The declaration does not prove full Regge convergence without any conditions; the curvature bound and mesh threshold remain. It does not establish strong-field convergence without an additional bounded-curvature assumption. It does not claim the cubic lattice is the only lattice on which convergence holds.

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: