cms_theorem_5_1_measure_bound
plain-language theorem explainer
Scalar real abstraction of Cheeger–Müller–Schrader Theorem 5.1: the absolute gap between smooth and piecewise-flat curvature measures on a region U is at most c times (Vol(U)·√η plus the √η-tube volume of ∂U). Gravity and Regge-convergence modules cite it as the honest CMS-style input, separate from stronger O(a²) action hypotheses. It is a Prop definition, not a proved estimate.
Claim. The proposition asserting that for all real scalars $R_i(U)$, $R_{i,\eta}(U)$, $\mathrm{Vol}(U)$, $\mathrm{Vol}(B_{\sqrt{\eta}}(\partial U))$, mesh size $\eta$, and constant $c$, if $\mathrm{Vol}(U)\ge 0$, the boundary-tube volume is nonnegative, $0<\eta<1$, and $c>0$, then $|R_i(U)-R_{i,\eta}(U)|\le c\bigl(\mathrm{Vol}(U)\sqrt{\eta}+\mathrm{Vol}(B_{\sqrt{\eta}}(\partial U))\bigr)$.
background
The module records convergence inputs for passing from Regge calculus to Einstein–Hilbert geometry. A 2026 correction (after Beltracchi) separates what CMS actually proves from stronger lattice claims: CMS Theorem 5.1 is a curvature-measure bound with an $\eta^{1/2}$ bulk term plus a boundary-tube term, not a plain $|S_{\mathrm{Regge}}-S_{\mathrm{EH}}|\le C a^2$ statement.
The six real parameters are placeholders for geometric quantities on a smooth Riemannian manifold $M$ with a sufficiently fine $\Theta$-fat triangulation of mesh $\eta$ and a submanifold $U$ with smooth boundary: $R_i(U)$ the smooth Lipschitz–Killing curvature measure, $R_{i,\eta}(U)$ the piecewise-flat/Regge measure, $\mathrm{Vol}(U)$, the volume of the $\sqrt{\eta}$-tubular neighborhood of $\partial U$, mesh $\eta$, and a constant $c$ depending on curvature bounds and fatness.
Literature anchors are Cheeger–Müller–Schrader (1984) for measure convergence and Gentle–Miller (1998) for special second-order rates. This definition is the general CMS-shaped input; a sibling hypothesis packages the stronger quadratic rate used by some weak-field modules.
proof idea
No proof: this is a bare Prop abbreviation. The body is a single universal quantifier over six reals with the five positivity/mesh side conditions, then the absolute-value inequality with bulk $\mathrm{Vol}\cdot\sqrt{\eta}$ plus boundary-tube term. Downstream structures simply store a term of this type as a field (package form, certificate, registry).
why it matters
It is the canonical CMS 5.1-shaped interface for RS gravity convergence. CMSTheorem51 packages it as a structure field; RSReggeConvergence requires it as general curvature-measure convergence alongside optional stronger action/Ricci/Riemann axioms, tying Regge $J$-cost lattices to the Einstein–Hilbert integral with $\kappa_{\mathrm{RS}}=8\varphi^5$. NonlinearConvergenceCert threads it through vanishing lemmas for the bulk and full bound as $\eta\to 0$.
The registry layer (ReggeConvergenceRegistry.mk, cms_measure_bound_faithful) treats a proof of this Prop as the faithful CMS measure-bound slot, keeping provenance separate from the special quadratic hypothesis. That split prevents citing CMS for $O(a^2)$ action rates the literature does not give in full generality. In the RS chain it supports the continuum limit of discrete recognition geometry toward GR, without claiming a new analytic theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.