error_vanishes
plain-language theorem explainer
Second-order error terms of the form C a squared vanish in the continuum limit for any positive real C. Researchers formalizing discrete gravity approximations cite this to confirm that mesh-size discrepancies disappear when recovering the Einstein-Hilbert action. The argument proceeds by establishing continuity of the quadratic map and invoking preservation of limits under continuous functions.
Claim. Let $C > 0$ be a real constant. Then the limit of $C a^2$ as $a$ approaches 0 equals 0.
background
The module axiomatizes the Cheeger-Müller-Schrader convergence of Regge calculus to general relativity, where the discrete action on a simplicial lattice approaches the Einstein-Hilbert action at order a squared in the mesh size. Upstream results supply the RS coupling kappa equal to eight times phi to the fifth and the Einstein-Hilbert action as the integral of scalar curvature times the volume element. In the Recognition Science setting, J-cost minimization on recognition events supplies the discrete ledger whose continuum limit must recover the Einstein field equations.
proof idea
The proof first asserts continuity of the map a maps to C times a squared. It then applies the tendsto property of continuous functions at the point zero. Simplification reduces the goal to the known vanishing of a squared at zero, which is discharged directly.
why it matters
The result is invoked inside the nonlinear convergence certificate to verify that error terms vanish, thereby completing the bridge from the discrete RS ledger to the full nonlinear Einstein field equations. It supports the framework claim that J-cost minimization yields the Einstein-Hilbert action in the limit, conditional on the second-order convergence axioms. It touches the open question of replacing the axiomatized Cheeger-Müller-Schrader result by a full Mathlib formalization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.