mk_cms_measure_bound
plain-language theorem explainer
Projecting the CMS curvature-measure field from a Regge convergence registry built by the standard constructor recovers the original CMS Theorem 5.1 proposition unchanged. Anyone treating the registry as a faithful packaging of external curvature inputs cites this. The proof is pure definitional equality (`rfl`).
Claim. Let $h_1$ be the CMS Theorem 5.1 curvature-measure bound, $h_2$ the special quadratic Regge-to-Einstein-Hilbert convergence hypothesis, $h_3$ the Regge Ricci $O(a^2)$ convergence axiom, $h_4$ the Regge Riemann/holonomy convergence axiom, and $p$ a provenance list. If $R$ is the registry constructed from $(h_1,h_2,h_3,h_4,p)$, then the CMS measure-bound field of $R$ equals $h_1$.
background
The module ReggeConvergenceRegistry consolidates four external convergence propositions from NonlinearConvergence into one named structure. It is a faithful repackaging only: each field is typed by the original proposition, and no convergence content is restated or re-proved.
The CMS field is the Cheeger–Müller–Schrader (1984) Theorem 5.1 shape: for a smooth Riemannian manifold, a sufficiently fine $\Theta$-fat triangulation of mesh $\eta$, and a submanifold $U$ with smooth boundary, $$|R_i(U)-R_{i,\eta}(U)|\le c\bigl(\mathrm{Vol}(U)\sqrt{\eta}+\mathrm{Vol}(B_{\sqrt{\eta}}(\partial U))\bigr).$$ The other three inputs are stronger special-purpose hypotheses (quadratic action convergence, Ricci scalar $O(a^2)$, holonomy/Riemann $O(a^4)$ remainder), each axiomatized rather than derived inside the monolith.
The constructor mk assembles all four propositions plus a string provenance list into one registry value.
proof idea
One-line term proof by rfl. The constructor stores $h_1$ verbatim in the CMS measure-bound field, so projecting that field is definitionally equal to the input hypothesis. No lemmas are applied.
why it matters
This is one of the four faithful-projection theorems that certify the registry does not alter external mathematics. Downstream gravity developments that consume a single ReggeConvergenceRegistry (rather than four scattered axioms) can project out the CMS measure bound and know they hold exactly the Cheeger–Müller–Schrader input, not a restatement.
In the Recognition Science gravity stack, Regge calculus supplies the discrete curvature side of continuum limits. Packaging CMS Theorem 5.1 separately from the stronger quadratic and component-level axioms keeps the general measure estimate distinct from special weak-field hypotheses. No downstream consumers are wired yet (used_by is empty); the lemma exists so future continuum-limit arguments can cite a single registry without losing provenance or strength of the CMS bound.
It does not advance the forcing chain (T0–T8) or the Recognition Composition Law; it is infrastructure for the gravity/Regge layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.