Gravity Regge Convergence Registry

The convergence registry

Regge calculus is a way to compute gravity on a discrete grid, replacing smooth spacetime with a network of flat pieces, like a geodesic dome approximating a sphere. A central question is whether this discrete model converges to the smooth theory of general relativity as the grid is refined. The registry, a structured collection of four separate convergence results, consolidates the external mathematics that answers this question into one named object.

The four inputs come from different sources. One is a result by Cheeger, Müller, and Schrader from 1984, which bounds how curvature measures converge with a term involving the square root of the grid scale. The other three are hypotheses, not theorems: a stronger quadratic convergence assumption for special weak-field settings, a quadratic convergence statement for the Ricci scalar, and a similar one for the Riemann curvature. Each is an external mathematical result, and the registry records this status explicitly in its provenance field.

The registry does not prove or reprove any of these results. It repackages them faithfully. Each of the four fields in the structure is typed by the exact original proposition, and the library proves that projecting a field out of the registry recovers the original proposition. Building a registry from the four original proofs and then projecting them back gives you exactly what you started with, a round-trip property that confirms nothing was weakened in the repackaging.

In plain terms, the registry establishes that a discrete gravity computation can be trusted to approach smooth general relativity under the stated conditions, and it does so by organizing the evidence in a single, auditable place. This matters because the framework builds on the idea that reality keeps a discrete record of events, and Regge calculus is the natural mathematical language for that discreteness. The registry is the bridge that connects the discrete picture to the classical continuum limit, and it makes the provenance of that bridge explicit.

/-- A registry that consolidates the four external convergence Propositions
from `NonlinearConvergence` into a single named structure.

Each field is typed by the **exact** original proposition, so this is a
faithful repackaging, not a weakening.  The `provenance` field documents
each input as an external-mathematics result with a status tag. -/
structure ReggeConvergenceRegistry where
  /-- CMS Theorem 5.1 curvature-measure bound (Cheeger–Müller–Schrader 1984). -/
  cms_measure_bound : cms_theorem_5_1_measure_bound
  /-- Special-purpose `O(a²)` action-convergence hypothesis. -/
  special_quadratic : special_quadratic_regge_to_eh_convergence_hypothesis
  /-- Regge Ricci-scalar convergence axiom. -/
  ricci_convergence : regge_ricci_convergence_axiom
  /-- Regge Riemann / holonomy convergence axiom. -/
  riemann_convergence : regge_riemann_convergence_axiom
  /-- Documentation of each external-math result with a status tag. -/
  provenance : List String

/-- The `cms_measure_bound` field of a registry is a proof of the original
`cms_theorem_5_1_measure_bound` proposition from `NonlinearConvergence`. -/
theorem cms_measure_bound_faithful (r : ReggeConvergenceRegistry) :
    cms_theorem_5_1_measure_bound := r.cms_measure_bound

/-- The `special_quadratic` field of a registry is a proof of the original
`special_quadratic_regge_to_eh_convergence_hypothesis` proposition. -/
theorem special_quadratic_faithful (r : ReggeConvergenceRegistry) :
    special_quadratic_regge_to_eh_convergence_hypothesis := r.special_quadratic

/-- The `ricci_convergence` field of a registry is a proof of the original
`regge_ricci_convergence_axiom` proposition. -/
theorem ricci_convergence_faithful (r : ReggeConvergenceRegistry) :
    regge_ricci_convergence_axiom := r.ricci_convergence

/-- The `riemann_convergence` field of a registry is a proof of the original
`regge_riemann_convergence_axiom` proposition. -/
theorem riemann_convergence_faithful (r : ReggeConvergenceRegistry) :
    regge_riemann_convergence_axiom := r.riemann_convergence

/-- Building a registry from the projections of `r` recovers `r`.
This confirms the registry is a faithful repackaging. -/
theorem mk_roundtrip (r : ReggeConvergenceRegistry) :
    mk r.cms_measure_bound r.special_quadratic r.ricci_convergence
       r.riemann_convergence r.provenance = r := rfl

What this page does not claim

The registry does not prove that Regge calculus converges to general relativity. The registry does not derive the Cheeger-Müller-Schrader theorem. The registry does not claim the three hypotheses are theorems.

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