IndisputableMonolith.Gravity.ReggeConvergenceRegistry
Registry packaging the four external Regge-to-Einstein-Hilbert convergence propositions (CMS measure bound, special quadratic, Ricci, Riemann) into one named structure with exact types and provenance tags. Gravity authors cite it when they need a single handle on the nonlinear continuum limit inputs rather than four loose hypotheses. The module is pure structure assembly: faithful field-by-field repackaging, no new analysis.
claimA structure $\mathrm{ReggeConvergenceRegistry}$ whose fields are exactly the four external convergence propositions from the nonlinear Regge $\to$ Einstein-Hilbert limit (CMS measure bound, special-quadratic estimate, Ricci convergence, Riemann convergence), each typed by its original statement, together with a provenance record tagging each input as external mathematics.
background
Regge calculus discretizes spacetime by piecewise-flat simplicial complexes; the continuum limit should recover the Einstein-Hilbert action and its curvature tensors. The sibling module NonlinearConvergence records the analytic inputs for that passage: bounds on the CMS measure, a special quadratic estimate, and convergence statements for Ricci and Riemann curvature under mesh refinement.
Those four statements are treated as external mathematics (results from the literature, not proved inside the monolith). The 2026-05-13 correction note in the upstream module emphasizes that comments must not overstate what CMS actually proves; the registry inherits that discipline by keeping each field typed to the exact original proposition.
This module sits in the Gravity domain and imports only Mathlib plus that nonlinear-convergence record. It introduces no new analytic content: it names a single structure so downstream gravity developments can depend on one object rather than four free-floating hypotheses.
proof idea
This is a definition module, no proofs of convergence. It declares a structure whose fields are the four external propositions with identical types (faithful, not weakened), plus a provenance field. Constructor helpers (mk, field-wise mk_*, mk_provenance, mk_roundtrip) assemble and round-trip instances. Faithfulness lemmas record that each projected field matches the source proposition.
why it matters in Recognition Science
In Recognition Science gravity work, the continuum limit of the discrete (Regge) action is the bridge from combinatorial recognition geometry to classical Einstein-Hilbert dynamics. Bundling the four external convergence inputs into one registry makes that bridge auditable: every consumer sees the same typed hypotheses and the same external-math provenance tags.
No downstream monolith theorems are wired yet (used_by is empty); the module is infrastructure for future gravity developments that need a single, non-weakened package of Regge convergence assumptions. It does not itself advance the forcing chain (T0-T8) or the Recognition Composition Law; it only organizes the classical geometric limit data those gravity layers will eventually cite.
scope and limits
- Does not prove any Regge-to-Einstein-Hilbert convergence theorem.
- Does not weaken or strengthen the four external propositions; types are exact copies.
- Does not derive CMS, Ricci, or Riemann estimates inside Lean.
- Does not connect yet to RS forcing chain steps T0-T8 or mass/ladder formulae.
- Does not assert physical validity of the external literature results it packages.
depends on (1)
declarations in this module (13)
-
structure
ReggeConvergenceRegistry -
theorem
cms_measure_bound_faithful -
theorem
special_quadratic_faithful -
theorem
ricci_convergence_faithful -
theorem
riemann_convergence_faithful -
def
mk -
theorem
mk_cms_measure_bound -
theorem
mk_special_quadratic -
theorem
mk_ricci_convergence -
theorem
mk_riemann_convergence -
theorem
mk_provenance -
theorem
mk_roundtrip -
def
defaultProvenance