quadratic_error_vanishes
plain-language theorem explainer
For any fixed positive constant C, the quadratic error C a² tends to 0 as the mesh scale a tends to 0. Gravity and lattice-GR modules cite this to turn an O(a²) Regge-to-Einstein-Hilbert rate into an actual limit statement. The proof is a one-shot continuity argument at the origin.
Claim. For every real constant $C>0$, $\lim_{a\to 0} C a^{2}=0$ in the usual topology on $\mathbb{R}$ (equivalently, $a\mapsto C a^{2}$ tends to $0$ along neighborhoods of $0$).
background
The module records inputs for passing from Regge calculus (piecewise-flat simplicial gravity) to continuum Einstein-Hilbert geometry. After a 2026 correction, it carefully separates Cheeger-Müller-Schrader Theorem 5.1 (a curvature-measure bound with an $\eta^{1/2}$ bulk term plus a boundary-tube term) from a stronger special hypothesis that the action or curvature error is genuinely $O(a^{2})$.
That stronger rate is the setting here: once one has an error controlled by $C a^{2}$ for fixed $C>0$, one still needs the elementary analytic fact that the quadratic itself vanishes in the continuum limit $a\to 0$. No Recognition-Science constants ($\phi$, eight-tick structure, etc.) enter; this is pure real analysis supporting the gravity convergence layer.
proof idea
Show that $a\mapsto C a^{2}$ is continuous on $\mathbb{R}$ (Mathlib continuity). Continuous maps send filters to filters, so the map tends to its value at $0$. Simplification reduces that value to $0$, which is the claimed Tendsto into nhds 0. The positivity hypothesis on $C$ is unused in the argument; it is carried only for API uniformity with the surrounding $O(a^{2})$ bounds.
why it matters
Downstream, error_vanishes is a backward-compatible alias that simply applies this theorem, so older call sites keep compiling under the corrected CMS-versus-special-quadratic split. In the broader file, this closes the last analytic step of the special (not CMS-general) second-order path: once a module assumes or proves an $O(a^{2})$ Regge-to-EH discrepancy, the continuum limit of that discrepancy is automatic.
It does not itself establish Regge calculus convergence in RS gravity; it only converts a quadratic rate into a vanishing statement. The genuine geometric content remains either the CMS measure bound or the named special quadratic hypothesis used by weak-field and numerical lattice modules.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.