cms_bound_vanishes
plain-language theorem explainer
Whenever the CMS Theorem 5.1 boundary-tube volume tends to zero with the mesh parameter η, the full right-hand side of that curvature-measure bound also tends to zero. Gravity and discrete-geometry workers citing Regge-to-Einstein-Hilbert measure convergence use this closure step. The argument is elementary filter arithmetic: continuous square root at zero, constant multiplications, and addition of the given boundary tendsto.
Claim. Let $C,\mathrm{Vol}(U)\in\mathbb{R}$ and let $v:\mathbb{R}\to\mathbb{R}$ satisfy $v(\eta)\to 0$ as $\eta\to 0$. Then $C\bigl(\mathrm{Vol}(U)\,\sqrt{\eta}+v(\eta)\bigr)\to 0$ as $\eta\to 0$.
background
This module records the analytic inputs needed to pass from Regge calculus to Einstein-Hilbert geometry. After a 2026 correction, it carefully separates what Cheeger-Müller-Schrader actually prove from a stronger special-purpose quadratic rate.
CMS Theorem 5.1 (Cheeger's 2016 notation) is a curvature-measure bound $|R_i(U)-R_{i,\eta}(U)|\le c\bigl(\mathrm{Vol}(U),\eta^{1/2}+\mathrm{Vol}(B_{\eta^{1/2}}(\partial U))\bigr)$. The bulk term is only square-root in the mesh scale; a boundary-tube volume appears separately. That is measure convergence, not a plain $O(a^2)$ action error.
The present lemma is the elementary continuum-limit closure for that full right-hand side once the boundary-tube contribution is known to vanish. A sibling lemma already handles the pure bulk $\sqrt{\eta}$ piece.
proof idea
Three short filter steps. First, continuity of $\sqrt{\cdot}$ at $0$ gives $\sqrt{\eta}\to 0$; multiply by the constant $\mathrm{Vol}(U)$ via constant tendsto and product of limits. Second, add the hypothesis that the boundary-tube volume tends to $0$, obtaining tendsto of the sum to $0+0$. Third, multiply by the constant $C$ and rewrite with the distributive law so the target expression matches. All steps are standard Tendsto algebra in the neighborhood filter of $0$.
why it matters
The lemma is wired into the module certificate nonlinear_convergence_cert as the field that asserts the full CMS right-hand side vanishes. That certificate packages the corrected CMS measure-bound story separately from the stronger special quadratic Regge-to-EH hypothesis used by some weak-field or lattice modules.
In the Recognition gravity stack this is bookkeeping, not new physics: it lets downstream code cite a proved continuum-limit vanishing for the CMS-style bound without overclaiming $O(a^2)$ from CMS alone. The module doc is explicit that Gentle-Miller-type second-order rates live under a different hypothesis interface. No forcing-chain landmark (T0-T8, RCL, phi) is touched; the result is pure analysis supporting the Regge continuum limit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.