Gravity Regge Convergence Registry Cms Measure Bound Faithful

The convergence registry

In numerical relativity, Regge calculus approximates spacetime by a simplicial grid, and a central question is whether the discrete geometry converges to the smooth continuum as the grid spacing shrinks. A 1984 theorem by Jeff Cheeger, Werner Müller, and Robert Schrader (CMS) established a curvature-measure convergence bound for such settings. The Recognition Science framework's ledger, a discrete record of events, houses a machine-checked library of formal theorems that consolidates this external result into a single structure called the Regge convergence registry.

The declaration cms_measure_bound_faithful proves that the registry's field for the CMS bound is exactly the original proposition, not a weakened or altered version. The theorem states that for any registry value r, the field r.cms_measure_bound is a proof of cms_theorem_5_1_measure_bound, the precise CMS Theorem 5.1 statement. This is a faithful repackaging: the registry does not restate or re-prove convergence content, it merely references the existing proposition. The registry also holds three other convergence inputs, each documented with a status tag, and the faithful-projection theorems show that every field recovers its original proposition.

What the declaration does not claim is equally important. It does not prove the CMS theorem itself; that 1984 result is an external theorem, axiomatized into the framework. The registry does not establish that Regge calculus converges in general, only that the named structure packages the external convergence assumptions without weakening them. The other three registry fields are external hypotheses, not theorems: the special quadratic action-convergence hypothesis, the Regge Ricci-scalar convergence axiom, and the Regge Riemann or holonomy convergence axiom. Each carries a status tag in the provenance list, and the faithful-projection theorems confirm the registry is a faithful repackaging, not a new mathematical result.

The practical consequence is that the framework can organize external convergence results into a named, machine-checked structure while preserving their exact logical content. Researchers can build a registry from proofs of the four original propositions, and the round-trip theorem shows that projecting and rebuilding recovers the original registry. This gives the framework a clean interface for working with external mathematics, with provenance recorded and faithfulness guaranteed by the kernel-checked theorems.

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

/-- 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 `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 declaration does not prove the CMS theorem itself; it only packages the external result. The registry does not establish that Regge calculus converges in general. The other three registry fields are external hypotheses, not 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: