NonlinearConvergenceCert
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.
claimA 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 in Recognition Science
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.
scope and limits
- Does not derive the Schläfli identity or Cayley-Menger determinants.
- Does not bound curvature error in terms of mesh quality.
- Does not extract convergent subsequences via compactness.
- Does not replace the axiomatized convergence with a complete proof.
Lean usage
theorem nonlinear_convergence_cert : NonlinearConvergenceCert where second_order := fun _ _ _ => convergence_is_second_order _ (by linarith) (by linarith) error_goes_to_zero := error_vanishes kappa := rs_kappa_valueformal statement (Lean)
159structure NonlinearConvergenceCert where
160 second_order : ∀ a : ℝ, 0 < a → a < 1 → (a/2)^2 = a^2/4
161 error_goes_to_zero : ∀ C : ℝ, 0 < C →
162 Filter.Tendsto (fun a => C * a ^ 2) (nhds 0) (nhds 0)
163 kappa : rs_kappa = 8 * phi ^ 5
164