Gravity Cubic Regge Convergence Cubic Convergence Cert

The convergence certificate

In numerical physics, when you replace a smooth continuum by a discrete grid, you want to know that the grid version approaches the true theory as the grid gets finer. The declaration cubic_convergence_cert is a formal, machine-checked statement that for the Recognition Science cubic lattice, this convergence happens at a rate proportional to the square of the grid spacing, a standard and desirable second-order behavior. The certificate bundles four separate facts that together support this conclusion.

The first fact is that the cubic lattice has perfect shape quality: every cell is an identical cube, so a regularity condition that general triangulations must impose is automatically satisfied. The second is that the lattice carries a natural shortest wavelength, the 8-tick period, which acts as a physical cutoff that prevents the ultraviolet divergences that plague continuum quantum gravity. The third is that the golden ratio phi is greater than 1, which implies that the lattice resolution grows exponentially with refinement level, outpacing any polynomial growth in the number of points. The fourth is the convergence estimate itself: for any sufficiently smooth field, the error between the lattice second difference and the true second derivative is bounded by a constant times the square of the spacing.

In the weak-field regime, where field variations are small, this convergence is unconditional: the estimate holds for any smooth field without further assumptions. The certificate records this as a universal statement over all smooth functions. In the strong-field regime, the certificate is more cautious. It does not assert unconditional convergence; instead it states that convergence holds conditional on a bound on the curvature, a standard requirement in Regge calculus. The certificate also notes that the shape-quality condition, one of the three conditions in the general Cheeger-Müller-Schrader theorem, is free for the cubic lattice, removing one obstacle to convergence.

What the certificate does not claim is as important as what it proves. It does not prove that the lattice action equals the continuum action at any finite spacing; it proves a bound on the difference that shrinks as the spacing goes to zero. It does not establish convergence for arbitrary non-smooth fields or for strong fields without a curvature bound. And it does not claim that the 8-tick cutoff is the physically correct one for quantum gravity; it only records that the lattice has a natural cutoff. The certificate is a precise, scoped statement about a specific lattice construction, not a general proof that this discrete gravity theory is the correct description of nature.

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

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

/-- The cutoff is positive. -/
theorem uv_cutoff_pos : 0 < uv_cutoff := by
  unfold uv_cutoff
  positivity

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

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

What this page does not claim

The certificate does not prove that the lattice action equals the continuum action at any finite spacing. It does not establish convergence for non-smooth fields or for strong fields without a curvature bound. It does not claim that the 8-tick cutoff is the physically correct cutoff 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: