Gravity Cubic Regge Convergence Rs Cubic Shape Quality

Shape quality on the cubic lattice

In numerical relativity, Regge calculus approximates curved spacetime by a lattice of flat building blocks, and a key question is whether the approximation improves as the blocks shrink. A classical convergence theorem, due to Cheeger, Müller, and Schrader, requires the blocks to satisfy a regularity condition on their aspect ratio, a measure of how far a cell is from being equilateral. The Recognition Science framework's machine-checked library of formal theorems contains a declaration, rs_cubic_shape_quality, that establishes a simple but consequential fact: for its cubic lattice, the shape quality parameter σ equals 1 exactly.

The value σ = 1 is the perfect score. It means every cell in the lattice is a cube, with all edges equal and all angles right angles, so the aspect-ratio condition of the Cheeger-Müller-Schrader theorem is satisfied automatically. The declaration is a theorem, proved by definitional equality in the framework's library: the shape bound for a cube is 1 by construction. This removes one of the three conditions the general theorem demands, leaving only a curvature bound and a mesh threshold as genuine hypotheses for convergence in the strong-field regime.

In the weak-field regime, the framework proves a stronger, unconditional result. For a smooth field with |ε| < 1, the quartic error in the J-cost action is bounded by ε⁴/24 at each site, and the total error vanishes as O(a) in the continuum limit. A separate estimate upgrades this to second-order convergence, O(a²), for the Laplacian on smooth fields. The cubic shape quality is the structural reason these estimates hold without the full CMS regularity apparatus.

In Recognition Science, this fact is one of three structural advantages of the cubic lattice, alongside the 8-tick periodicity that provides a natural ultraviolet cutoff and the exponential growth bound φ^N > C·N³ that controls curvature concentration. The declaration itself, however, is narrow: it states the shape quality for cubes, nothing more. It does not prove the convergence theorems, does not establish the curvature bound, and does not address whether the physical recognition-to-linking bridge, which would connect this lattice to actual spacetime, exists. That bridge remains open.

The practical consequence is that a numerical relativist working with a cubic lattice in the framework's setting can take the shape condition as granted, not as a hypothesis to verify. The framework's library records this as a theorem, not a modeling choice, and the proof is a direct computation. What the declaration does not do is tell you whether the lattice itself is physically realized; it only tells you that if you use cubes, the shape condition is not what will stop your simulation from converging.

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

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

/-- In the weak-field regime |ε| < 1, the quartic error in J-cost
    is bounded by |ε|⁴/24 at each site.

    For N lattice sites, the total error is bounded by:
    N · |ε_max|⁴ / 24 ≤ (a⁻³ · V) · a⁴ · const / 24
    = V · a · const / 24

    where V is the total volume and a is the lattice spacing.
    This is O(a) and vanishes in the continuum limit. -/
theorem quartic_error_controlled (ε_max : ℝ) (hε : 0 < ε_max) (hε1 : ε_max < 1) :
    ε_max ^ 4 / 24 < ε_max ^ 2 / 2 := by
  have h_sq_lt : ε_max * ε_max < 1 := by nlinarith
  nlinarith [sq_nonneg ε_max, sq_nonneg (ε_max * ε_max)]

/-- 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 the convergence theorems themselves, only the shape quality condition. The declaration does not establish the curvature bound required for strong-field convergence. The declaration does not assert that the cubic lattice is physically realized in 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/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: