Gravity Regge Convergence Registry Mk Cms Measure Bound

A registry for convergence

In numerical relativity, Regge calculus approximates spacetime by a network of flat simplexes, and a central question is whether the discrete geometry converges to the continuous Einstein theory as the network is refined. The declaration mk_cms_measure_bound belongs to a small formal structure in the Recognition Science framework's machine-checked library of formal theorems that gathers four such convergence statements into one package, the ReggeConvergenceRegistry. The first of these is the Cheeger–Müller–Schrader (1984) Theorem 5.1 bound on curvature-measure convergence, which controls how the discrete curvature measure approaches the continuum one at a rate of η^(1/2) plus a boundary-tube term. The other three are hypotheses of faster convergence used in special weak-field or numerical settings.

The theorem mk_cms_measure_bound states that when a registry is built from a proof of the original CMS bound, extracting the cms_measure_bound field from that registry recovers exactly that same proof. This is a round-trip property: the registry is a faithful repackaging, not a weakening or a re-statement. The proof is by definitional equality, meaning the act of constructing the registry and then projecting out the field is literally the identity operation on the proof object. Four analogous theorems cover the other three fields, and a fifth, mk_roundtrip, shows that building a registry from the projections of any registry recovers the original registry.

The declaration establishes only this bookkeeping fact. It does not prove the CMS bound itself, nor any of the three convergence hypotheses. Those are external-mathematics results, axiomatized in the library with explicit provenance tags: one external theorem and three external hypotheses. The registry's purpose is organizational, to consolidate scattered references under one named structure, and the faithful-projection theorems certify that the consolidation preserves the exact original statements. This matters because it lets later formal work refer to a single registry instead of four separate propositions, with the assurance that nothing was lost in the packaging.

/-- Projecting the `cms_measure_bound` field of a registry built via `mk`
recovers the original proof. -/
theorem mk_cms_measure_bound
    (h1 : cms_theorem_5_1_measure_bound)
    (h2 : special_quadratic_regge_to_eh_convergence_hypothesis)
    (h3 : regge_ricci_convergence_axiom)
    (h4 : regge_riemann_convergence_axiom)
    (prov : List String) :
    (mk h1 h2 h3 h4 prov).cms_measure_bound = h1 := rfl

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

/-- The default provenance list documenting each external-math result
with a status tag. -/
def defaultProvenance : List String :=
  [ "cms_measure_bound: Cheeger–Müller–Schrader (1984), Theorem 5.1 — curvature-measure convergence; status: external theorem, axiomatized"
  , "special_quadratic: stronger O(a²) action-convergence hypothesis; status: external hypothesis, axiomatized"
  , "ricci_convergence: Regge Ricci-scalar O(a²) convergence; status: external hypothesis, axiomatized"
  , "riemann_convergence: Regge holonomy / Riemann convergence; status: external hypothesis, axiomatized" ]

What this page does not claim

The declaration does not prove the Cheeger–Müller–Schrader bound or any of the three convergence hypotheses. The registry does not state or re-prove any convergence content; it only repackages references to existing propositions. The theorem does not assert that Regge calculus converges to general relativity in any physical sense.

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: