mk
plain-language theorem explainer
Packages the four external Regge-to-continuum convergence inputs (CMS curvature-measure bound, special O(a²) action hypothesis, Ricci and Riemann axioms) plus a provenance list into one registry record. Gravity continuum-limit work cites it when assembling those hypotheses as a single object. The body is a pure structure constructor: each argument is assigned to the matching field.
Claim. Given a proof of the CMS Theorem 5.1 curvature-measure bound, a proof of the special $O(a^2)$ Regge-to-Einstein-Hilbert action-convergence hypothesis, proofs of the Regge Ricci-scalar and Regge Riemann/holonomy convergence axioms, and a provenance list of strings, form a Regge convergence registry whose four mathematical fields are exactly those inputs and whose provenance field is that list.
background
The module consolidates four external convergence propositions from NonlinearConvergence into one named structure. Each field is typed by the exact original proposition, so the registry is a faithful repackaging rather than a restatement or weakening of the continuum-limit content.
The four inputs are external mathematics: (1) Cheeger–Müller–Schrader (1984) Theorem 5.1, a curvature-measure estimate of the form $|R_i(U)-R_{i,\eta}(U)|\le c(\mathrm{Vol}(U)\sqrt{\eta}+\mathrm{Vol}(B_{\sqrt{\eta}}(\partial U)))$ for fine fat triangulations; (2) a stronger special-purpose $O(a^2)$ action-convergence hypothesis used in weak-field or numerical settings; (3) Regge Ricci-scalar convergence at $O(a^2)$; (4) Regge holonomy/Riemann convergence. All four are axiomatized as Props in the upstream module; none is re-proved here.
The registry also carries a string list documenting each input's external status. Sibling projection lemmas show that reading a field off a registry recovers the original proposition.
proof idea
Definitional structure constructor, not a proof. The four hypothesis arguments and the provenance list are assigned field-by-field to cms_measure_bound, special_quadratic, ricci_convergence, riemann_convergence, and provenance. No tactics, no lemmas, no rewriting: this is the converse direction of the faithful-projection theorems that unpack a registry back to the original propositions.
why it matters
In the Recognition gravity stack, discrete Regge geometry must meet continuum Einstein-Hilbert behavior under mesh refinement. Those continuum limits currently sit as four scattered external axioms. This constructor is the single entry point that bundles them into one named object so downstream gravity analysis can depend on a registry rather than four free-floating hypotheses.
The module doc is explicit: no convergence content is restated or re-proved; only references are repackaged. That keeps the external-math boundary sharp (CMS 1984 measure bound versus the stronger special $O(a^2)$ Ricci/Riemann hypotheses). Sibling mk_* helpers and the faithful-projection lemmas close the round-trip. No downstream consumers are wired yet (used_by is empty), so this is infrastructure for the nonlinear Regge convergence layer rather than a step in the T0–T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.