Gravity Nonlinear Convergence Error Vanishes

The vanishing error

The declaration error_vanishes is a small, precise statement about a limit. It says that for any positive constant C, the expression C times a squared quantity tends to zero as that quantity itself approaches zero. In symbols: as a goes to 0, C·a² goes to 0. This is a basic fact of calculus, and in the machine-checked library of formal theorems it is proved directly from the continuity of the squaring function.

The statement matters because of where it sits. In numerical approaches to general relativity, one often approximates a smooth curved spacetime by a lattice of flat pieces, an idea called Regge calculus. The approximation has an error that depends on the fineness of the lattice, often denoted a. The declaration error_vanishes is the formal anchor for the intuitive claim that this error disappears as the lattice gets finer. It is the endpoint of a chain: the error is bounded by C·a², and that bound goes to zero.

The declaration does not, by itself, establish that the error really is bounded by C·a². That bound comes from a separate, stronger hypothesis, called the special quadratic convergence hypothesis, which is an axiom in the library, not a proved theorem. The general theorem from Cheeger, Müller, and Schrader (1984) gives a weaker bound involving the square root of the mesh size plus a boundary term. The quadratic bound is a special-purpose assumption used in some weak-field or numerical settings. The declaration error_vanishes only takes that assumed bound and shows its limit is zero.

In Recognition Science, the framework models the Regge action as converging to the Einstein-Hilbert action, conditional on these convergence axioms. The framework's library records this as a structure that bundles the general measure convergence, the stronger quadratic action convergence, and a derived coupling constant. The full nonlinear Einstein field equations are described as following from the discrete ledger only if those convergence axioms hold. The declaration error_vanishes is the clean final step in that conditional story, not the proof of the story's premises.

/-- Backward-compatible old theorem name. -/
theorem error_vanishes (C : ℝ) (hC : 0 < C) :
    Filter.Tendsto (fun a => C * a ^ 2) (nhds 0) (nhds 0) :=
  quadratic_error_vanishes C hC

/-- **CMS Theorem 5.1 shape, scalar real abstraction.**

For a smooth Riemannian manifold `M`, a sufficiently fine `Θ`-fat
triangulation with mesh `η`, and a submanifold `U` with smooth boundary, CMS
prove a curvature-measure estimate of the form

`|R_i(U) - R_{i,η}(U)| ≤ c · (Vol(U) · sqrt η + Vol(B_{sqrt η}(∂U)))`.

The real variables here are the scalar placeholders for those geometric
quantities:

* `RiU`: smooth Lipschitz-Killing curvature measure on `U`;
* `RiEtaU`: piecewise-flat / Regge curvature measure on `U`;
* `VolU`: volume of `U`;
* `boundaryTubeVol`: volume of the `sqrt η`-tubular neighborhood of `∂U`;
* `η`: mesh size;
* `c`: the CMS constant depending on curvature bounds and fatness.

This is deliberately **not** an `O(η^2)` statement. -/
def cms_theorem_5_1_measure_bound : Prop :=
  ∀ (RiU RiEtaU VolU boundaryTubeVol η c : ℝ),
    0 ≤ VolU → 0 ≤ boundaryTubeVol → 0 < η → η < 1 → 0 < c →
      |RiU - RiEtaU| ≤ c * (VolU * Real.sqrt η + boundaryTubeVol)

/-- **Special stronger hypothesis (not CMS Theorem 5.1 in general).**

Some weak-field cubic-lattice or numerical Regge settings can carry
second-order truncation/convergence estimates.  That is a separate input from
the general CMS curvature-measure theorem above.

This is the old `regge_to_eh_convergence_axiom` statement, retained under a
more honest name. -/
def special_quadratic_regge_to_eh_convergence_hypothesis : Prop :=
  ∀ (S_EH : ℝ) (a : ℝ), 0 < a → a < 1 →
    ∃ (S_Regge : ℝ) (C : ℝ), 0 < C ∧
      |S_Regge - S_EH| ≤ C * a ^ 2

What this page does not claim

The declaration does not prove that the quadratic error bound itself holds. It does not establish convergence of Regge calculus to general relativity without additional axioms. It does not claim the full nonlinear Einstein field equations follow from the discrete ledger unconditionally.

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