RSReggeConvergence
plain-language theorem explainer
The convergence record bundles the Regge action convergence to the Einstein-Hilbert action, the associated Ricci scalar convergence at order a squared, the coupling constant equal to eight times phi to the fifth, and its positivity. Researchers in discrete approaches to gravity would cite it when deriving the continuum Einstein equations from a lattice model. It is introduced as a record that directly assembles these four properties.
Claim. The structure asserts that the Regge action on a simplicial lattice converges to the Einstein-Hilbert action with an error of order $a^2$ in the mesh size $a$, that the Regge Ricci scalar converges to the continuum Ricci scalar at the same order, that the gravitational coupling satisfies $k = 8 phi^5$, and that this coupling is positive.
background
The module axiomatizes the classical result that the Regge action on refined triangulations converges to the Einstein-Hilbert action. The action convergence axiom states that for a smooth metric the difference between the discrete action and the continuum integral of the scalar curvature is bounded by a constant times the square of the mesh size. The Ricci convergence axiom supplies the corresponding pointwise bound for the curvature scalar expressed as a sum of deficit angles.
proof idea
The declaration is a structure definition whose fields are filled directly by the two convergence axioms, the explicit equality for the coupling constant, and the positivity inequality. No additional lemmas or tactics are required.
why it matters
This record is consumed by the theorem that derives general relativity from the RS lattice once the convergence axioms are assumed. It thereby supplies the final link from the discrete J-cost ledger through Regge calculus to the full nonlinear Einstein field equations. The construction rests on the Cheeger-Müller-Schrader convergence theorem rather than proving it internally, leaving the formalization of that classical result as an open task.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.