cms_sqrt_bulk_vanishes
plain-language theorem explainer
The CMS bulk contribution C·Vol(U)·√η tends to 0 as the mesh scale η→0. Anyone assembling the full Cheeger–Müller–Schrader Theorem 5.1 right-hand side cites this elementary limit. The proof is continuity of square root at 0, then two constant multiplications in the filter topology.
Claim. For any real constants $C$ and $\mathrm{Vol}(U)$, the map $\eta \mapsto C \cdot \mathrm{Vol}(U) \cdot \sqrt{\eta}$ tends to $0$ as $\eta \to 0$ in the standard topology on $\mathbb{R}$.
background
This module records inputs for passing from Regge calculus to Einstein–Hilbert geometry. After a 2026 correction, CMS Theorem 5.1 is stated as 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)$,
not a plain $O(a^2)$ action error. The bulk piece is proportional to $\sqrt{\eta}$; the second summand is a boundary-tube volume.
The present lemma isolates the bulk factor: once $\eta\to 0$, the product of any fixed prefactor $C$, any fixed region volume $\mathrm{Vol}(U)$, and $\sqrt{\eta}$ vanishes. Continuity of $\sqrt{\cdot}$ at the origin is the only analytic input; the rest is filter arithmetic with constant nets.
proof idea
Three short filter steps. First, $\sqrt{\eta}\to 0$ as $\eta\to 0$ by continuity of Real.sqrt at 0. Second, multiply by the constant net $\mathrm{Vol}(U)$ via tendsto_const_nhds.mul. Third, multiply by the constant net $C$ the same way. A final simpa reassociates the product to match the claimed map.
why it matters
Feeds nonlinear_convergence_cert, which packages the CMS bulk vanishing, the full bound vanishing, and the stronger second-order hypothesis into one certificate for Regge→EH convergence in the gravity stack. Without the bulk term going to zero, the CMS 5.1 right-hand side cannot be driven to zero even if the boundary tube shrinks. In the Recognition Science gravity path this is bookkeeping for the continuum limit of the piecewise-flat action, not a new geometric theorem: the literature status is already recorded in the module header (CMS 1984; Gentle–Miller 1998 for special $O(a^2)$ cases). It sits beside the separated special quadratic hypothesis so downstream code no longer confuses the general measure bound with a second-order rate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.