Gravity Nonlinear Convergence Cms Sqrt Bulk Vanishes

The vanishing bulk term

Regge calculus is a way of approximating curved spacetime by gluing together flat pieces, much as a geodesic dome approximates a sphere with flat triangles. The approximation gets better as the pieces get smaller, and the mesh size, call it η, measures how small they are. A key question is how quickly the discrete curvature approaches the smooth curvature as η shrinks. In 1984, Jeff Cheeger, Werner Müller, and Robert Schrader proved a general bound: the difference between the smooth and discrete curvature measures is at most a constant times the volume of the region times the square root of η, plus a term for the volume of a thin tube around the boundary.

The declaration cms_sqrt_bulk_vanishes in the framework's machine-checked library of formal theorems is a small piece of that story. It states, formally, that the bulk term, the constant times the volume times the square root of η, tends to zero as η tends to zero. This is a simple fact from calculus: the square root of a tiny number is itself tiny. The theorem is not about physics directly; it is a formal verification that one part of the CMS bound, the part that does not involve the boundary, disappears in the limit of a fine mesh.

The declaration does not claim that the whole CMS bound vanishes. That would also require the boundary-tube term to vanish, which is a separate condition. The library states that separately in a theorem called cms_bound_vanishes, which assumes the boundary tube volume also goes to zero. And importantly, cms_sqrt_bulk_vanishes says nothing about the rate of convergence. The CMS bound is a square-root rate, not a quadratic one. A stronger quadratic rate, where the error is bounded by a constant times η squared, is a separate, special-purpose hypothesis in the library, not a consequence of the general CMS theorem.

The distinction matters because the framework uses these convergence inputs to connect its discrete lattice model of gravity to the standard Einstein equations. The framework's library records the CMS result as an axiom, a labeled input, not as something it derives from first principles. The stronger quadratic convergence, which some numerical tests support, is also an axiom, kept separate and clearly labeled. The formal library thus keeps the honest, general theorem distinct from the stronger, special-case assumption, so that downstream results know exactly what they are resting on.

/-- The CMS bulk term `sqrt η` vanishes as `η -> 0`. -/
theorem cms_sqrt_bulk_vanishes (C VolU : ℝ) :
    Filter.Tendsto (fun η : ℝ => C * (VolU * Real.sqrt η)) (nhds 0) (nhds 0) := by
  have hsqrt : Filter.Tendsto (fun η : ℝ => Real.sqrt η) (nhds 0) (nhds 0) := by
    simpa using (Real.continuous_sqrt.tendsto 0)
  have hVol : Filter.Tendsto (fun η : ℝ => VolU * Real.sqrt η) (nhds 0) (nhds 0) := by
    have hconst : Filter.Tendsto (fun _ : ℝ => VolU) (nhds 0) (nhds VolU) :=
      tendsto_const_nhds
    simpa using hconst.mul hsqrt
  have hC : Filter.Tendsto (fun _ : ℝ => C) (nhds 0) (nhds C) := tendsto_const_nhds
  simpa using hC.mul hVol

/-- If the boundary-tube volume also vanishes as `η -> 0`, then the whole
CMS Theorem 5.1 right-hand side vanishes. -/
theorem cms_bound_vanishes
    (C VolU : ℝ) (boundaryTubeVol : ℝ → ℝ)
    (hBoundary : Filter.Tendsto boundaryTubeVol (nhds 0) (nhds 0)) :
    Filter.Tendsto
      (fun η : ℝ => C * (VolU * Real.sqrt η + boundaryTubeVol η))
      (nhds 0) (nhds 0) := by
  have hbulk : Filter.Tendsto (fun η : ℝ => VolU * Real.sqrt η) (nhds 0) (nhds 0) := by
    have hsqrt : Filter.Tendsto (fun η : ℝ => Real.sqrt η) (nhds 0) (nhds 0) := by
      simpa using (Real.continuous_sqrt.tendsto 0)
    have hconst : Filter.Tendsto (fun _ : ℝ => VolU) (nhds 0) (nhds VolU) :=
      tendsto_const_nhds
    simpa using hconst.mul hsqrt
  have hsum :
      Filter.Tendsto (fun η : ℝ => VolU * Real.sqrt η + boundaryTubeVol η)
        (nhds 0) (nhds (0 + 0)) := hbulk.add hBoundary
  have hC : Filter.Tendsto (fun _ : ℝ => C) (nhds 0) (nhds C) := tendsto_const_nhds
  simpa [mul_add] using hC.mul hsum

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

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

What this page does not claim

The declaration does not establish that Regge calculus converges to general relativity at a quadratic rate. The declaration does not prove that the boundary-tube term in the CMS bound vanishes. The declaration does not derive the Einstein field equations from the discrete lattice model.

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: