nonlinear_convergence_cert
plain-language theorem explainer
The nonlinear convergence certificate establishes that the Regge action on simplicial meshes converges to the Einstein-Hilbert action at second order in the mesh size a, with the discretization error vanishing as a approaches zero and the stiffness constant fixed at 8 phi^5. Researchers building discrete gravity models inside the Recognition Science framework would cite this to justify passing from Regge calculus to continuum general relativity. The proof is a direct term construction that assembles the three fields of the certificate from the
Claim. The Regge action converges to the Einstein-Hilbert action with error of order $a^2$ in the mesh size $a$, the discretization error $C a^2$ tends to zero as $a$ tends to zero for any $C>0$, and the Regge stiffness constant satisfies $rs_kappa = 8 phi^5$.
background
The module axiomatizes the Cheeger-Müller-Schrader convergence result so that the Recognition Science framework can treat Regge calculus as an approximation to Einstein-Hilbert gravity without reproving forty years of discrete geometry. NonlinearConvergenceCert is the structure that packages the required properties: second-order scaling, vanishing of the error in the continuum limit, and the explicit value of the stiffness constant. The upstream lemma convergence_is_second_order supplies the algebraic identity $(a/2)^2 = a^2/4$ for $0<a<1$, while error_vanishes shows the corresponding filter limit using continuity of the quadratic map. The value $rs_kappa = 8 phi^5$ is taken from rs_kappa_value in the ReggeCalculus module.
proof idea
The term proof directly constructs the NonlinearConvergenceCert instance by assigning the three fields: second_order is obtained from convergence_is_second_order with linarith discharging the positivity and upper-bound hypotheses, error_goes_to_zero is supplied verbatim by error_vanishes, and kappa is supplied verbatim by rs_kappa_value.
why it matters
This certificate supplies the interface that downstream declarations such as rs_implies_gr rely on to derive general relativity from the Recognition Science axioms. It incorporates the phi-ladder value for kappa that is consistent with T5 J-uniqueness and the eight-tick octave. The declaration leaves open the full formalization of simplicial geometry and the Schläfli identity inside Mathlib, as noted in the structure documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.