CMSTheorem51
plain-language theorem explainer
Package structure holding the CMS Theorem 5.1 curvature-measure bound as the general Regge-to-Einstein-Hilbert convergence input. Gravity modules that need the honest CMS estimate (not a plain O(a²) action bound) would cite it. One-field structure wrapping the measure-bound proposition; no proof content.
Claim. A package of the Cheeger–Müller–Schrader Theorem 5.1-style curvature-measure input: for curvature measures $R_i$ and piecewise-flat approximations $R_{i,\eta}$, $|R_i(U)-R_{i,\eta}(U)|\le c\cdot(\mathrm{Vol}(U)\cdot\eta^{1/2}+\mathrm{Vol}(B_{\eta^{1/2}}(\partial U)))$.
background
The module records convergence inputs used when passing from Regge calculus (piecewise-flat simplicial spacetime) to Einstein–Hilbert geometry. After a 2026 correction, the file separates the general CMS curvature-measure theorem from stronger special-purpose quadratic hypotheses.
CMS Theorem 5.1 (Cheeger 2016 notation) is a measure-convergence bound with an $\eta^{1/2}$ bulk term plus a boundary-tube term. It is not the same as a plain $|S_{\mathrm{Regge}}-S_{\mathrm{EH}}|\le C\cdot a^2$ estimate. The field measure_bound is exactly that CMS-style Prop: the general Riemannian curvature-measure convergence input.
Literature anchors are Cheeger–Müller–Schrader (1984) for curvature-measure convergence on piecewise-flat spaces, and Gentle–Miller (1998) for explicit second-order rates in special settings (those live under a separate sibling hypothesis).
proof idea
No proof: this is a one-field structure definition. It packages the already-declared proposition cms_theorem_5_1_measure_bound as a named bundle so downstream gravity code can take a single CMS-Theorem-5.1-style input rather than an anonymous Prop. Construction is just supplying a term of that measure-bound type.
why it matters
Keeps the Recognition gravity stack honest about what CMS actually supplies. The module doc records that earlier comments overstated CMS as an $O(a^2)$ theorem; this structure is the corrected general input, distinct from special_quadratic_regge_to_eh_convergence_hypothesis (the old regge_to_eh_convergence_axiom under a clearer name).
Downstream Regge-to-EH and nonlinear-convergence arguments that only need measure convergence should depend on this package rather than the stronger quadratic hypothesis. No used-by edges are recorded yet; the declaration is infrastructure for gravity modules that import NonlinearConvergence. It does not itself touch T0–T8, RCL, or the phi ladder; it is classical GR/Regge input sitting under the RS gravity layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.