NonlinearConvergenceCert
plain-language theorem explainer
The NonlinearConvergenceCert structure records three properties that certify second-order convergence of the Regge action to the Einstein-Hilbert action as mesh size a tends to zero, together with the identification of the RS stiffness constant. Discrete-gravity modelers and Recognition Science formalizers cite it when embedding the Cheeger-Müller-Schrader result without re-proving comparison geometry. The declaration is a plain record whose fields are later instantiated by separate algebraic and limit lemmas.
Claim. A certificate for nonlinear convergence of Regge calculus consists of: (i) the algebraic identity $∀ a ∈ ℝ, 0 < a < 1 → (a/2)^2 = a^2/4$; (ii) the filter limit $∀ C > 0, lim_{a→0} C a^2 = 0$; and (iii) the constant equality $κ_{RS} = 8 φ^5$, where $κ_{RS}$ is the stiffness inherited from the defect-to-metric map and $φ$ is the golden ratio.
background
The module axiomatizes the Cheeger-Müller-Schrader (1984) theorem that the Regge action on a refined simplicial complex converges to the Einstein-Hilbert action at order O(a²) in mesh size a. Upstream, rs_kappa is defined as 8 * phi^5 so that S_Regge → (1/2 κ) ∫ R √g d⁴x in the continuum limit. Related kappa definitions appear in thermal-conductivity and annular-cost modules, but here the value is fixed to the gravitational RS choice.
proof idea
The declaration is a structure definition that simply packages three independent assertions. The second_order field is the elementary quadratic identity. The error_goes_to_zero field is the standard nhds limit for any quadratic term. The kappa field directly copies the value 8 * phi^5 from rs_kappa. No tactics occur inside the structure; the fields are supplied later by the nonlinear_convergence_cert theorem via convergence_is_second_order and error_vanishes.
why it matters
This certificate supplies the interface that lets Recognition Science gravity axioms rest on the established Regge-to-Einstein-Hilbert convergence without a multi-year Mathlib formalization of simplicial geometry. It is consumed by the nonlinear_convergence_cert theorem. The construction closes the discrete phi-ladder description of matter to the continuum limit of general relativity, consistent with the eight-tick octave and D = 3. An open question is whether the full Cheeger-Müller-Schrader argument can be internalized in Lean.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.