rs_implies_gr
plain-language theorem explainer
If the RSReggeConvergence structure holds, the Regge action on the J-cost lattice converges to the Einstein-Hilbert action with error bounded by kappa times a squared for mesh size a between zero and one. Discrete gravity researchers cite this to justify replacing the continuum Einstein-Hilbert action with its Regge counterpart inside the Recognition Science framework. The declaration is a direct definition that packages the second-order convergence statement as a proposition.
Claim. Assume the structure asserting Regge action convergence to the Einstein-Hilbert action at order $a^2$ together with the coupling relation $kappa_{RS}=8phi^5$. The defined statement asserts that for all real $a$ with $0<a<1$ there exists a real error such that $|error|leq kappa_{RS} a^2$.
background
The module axiomatizes the Cheeger-Müller-Schrader convergence theorem, which states that the Regge action on a refined simplicial approximation converges to the Einstein-Hilbert action at order O(a^2) in the mesh size. RSReggeConvergence is the structure containing the action convergence axiom, the Ricci convergence axiom, the derived coupling kappa_RS equal to eight phi to the fifth, and the positivity of kappa. This allows the Recognition Science lattice, whose dynamics follow from J-cost minimization, to reproduce the Einstein field equations via the variational principle on the converged action. The local setting imports Regge calculus definitions that supply the discrete curvature expressions used in the axioms.
proof idea
The declaration is a definition that directly encodes the quantified error bound as the body of the proposition. No lemmas are applied; it serves as an interface that assumes the convergence axioms from the referenced structure.
why it matters
This definition bridges the discrete Regge calculus to the continuum general relativity within the Recognition Science framework. It enables derivation of the Einstein field equations from J-cost minimization on the lattice once the convergence axioms are granted. The module notes that a full proof would require simplicial geometry and comparison theorems not yet formalized in Mathlib, so the result remains an axiom package rather than a derived theorem. It touches the open question of formalizing Cheeger-Müller-Schrader in dependent type theory.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.