regge_to_eh_convergence_axiom
plain-language theorem explainer
The declaration defines an axiom asserting that the Regge action on refined triangulations converges to the Einstein-Hilbert action with an error bounded by C a squared for mesh size a. Researchers in discrete gravity and quantum gravity approaches would reference this to justify continuum limits in variational formulations. The definition directly encodes the quantified existence of the approximating Regge action and error constant without deriving it from more primitive statements.
Claim. For every real number $S_{EH}$ representing the Einstein-Hilbert action and every mesh size $a$ satisfying $0 < a < 1$, there exist a Regge action value $S_{Regge}$ and a positive constant $C$ such that the absolute difference $|S_{Regge} - S_{EH}|$ is at most $C a^2$.
background
This module axiomatizes the convergence of Regge calculus to general relativity, specifically the result from Cheeger, Müller, and Schrader (1984) that the Regge action converges to the Einstein-Hilbert action at second order in the mesh size. The local setting treats the Regge action as a discrete approximation on simplicial complexes and the Einstein-Hilbert action as the continuum integral of the scalar curvature. Key definitions include the mesh size parameter a, which controls the refinement of the triangulation, and the error bound that vanishes quadratically. Upstream results such as the structure of J-cost from PhiForcingDerived and ledger factorization provide the discrete foundation on which this convergence is imposed. The module documentation notes that this is not a new theorem but an axiomatization to allow the Recognition Science framework to build upon established Regge calculus literature without reproving it.
proof idea
The declaration is a direct definition of the proposition encoding the convergence statement. It quantifies over the Einstein-Hilbert action and mesh size, then asserts the existence of a Regge action and error constant satisfying the quadratic bound. No lemmas are applied; the definition serves as the interface for the Cheeger-Müller-Schrader result.
why it matters
This axiom supplies the action convergence component to the RSReggeConvergence structure, which in turn derives that J-cost minimization on the lattice implies the Einstein field equations via the Hilbert variation. It fills the gap between the discrete Recognition Science dynamics and continuum gravity, citing the Cheeger-Müller-Schrader theorem as the paper proposition. In the framework, it enables the transition from the phi-ladder and J-cost minimization to the standard general relativity limit at second order.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.