convergence_is_second_order
plain-language theorem explainer
The theorem confirms quadratic scaling of the discretization error under mesh refinement by proving the algebraic identity for squared mesh size. Researchers axiomatizing Regge calculus convergence to Einstein-Hilbert gravity would cite it to justify O(a^2) error bounds when halving the mesh size quarters the error. The proof is a direct one-line algebraic normalization over the reals.
Claim. For any real number $a$ satisfying $0 < a < 1$, the equality $(a/2)^2 = a^2/4$ holds.
background
The module axiomatizes the Cheeger-Müller-Schrader (1984) result that the Regge action on refined simplicial meshes converges to the Einstein-Hilbert action at second order in mesh size $a$. This supplies the concrete algebraic content for the second-order rate: halving $a$ quarters the error term. The upstream structure from ContinuumBridge.as identifies the discrete Laplacian action with the Regge curvature sum via weighted edge differences, providing the bridge that lets the O(a^2) scaling transfer to the continuum limit.
proof idea
The proof is a one-line wrapper that applies the ring tactic to normalize the polynomial identity over the reals.
why it matters
It directly populates the second_order field inside nonlinear_convergence_cert, which assembles the full NonlinearConvergenceCert record used by downstream gravity constructions. The declaration fills the explicit algebraic step in the module's axiomatization of the 1984 convergence theorem, allowing the Recognition Science framework to import established Regge-to-GR results without rederiving them. It touches the open question of replacing the axiom with a full Mathlib formalization of Cheeger-Müller-Schrader.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.