proof_requirements
plain-language theorem explainer
This definition enumerates the five mathematical ingredients required to derive Regge-to-Einstein-Hilbert convergence inside Lean. Researchers formalizing discrete gravity would cite it when deciding whether to axiomatize or prove the Cheeger-Müller-Schrader theorem. The body is a static list of strings with no proof tactics or computational reduction.
Claim. The prerequisites for a formal proof that the Regge action on refined triangulations converges to the Einstein-Hilbert action at order $O(a^2)$ are: simplicial geometry via Cayley-Menger determinants, the Schläfli identity, comparison geometry between smooth and piecewise-flat metrics, curvature error bounds, and compactness arguments for subsequence extraction.
background
The module axiomatizes the Cheeger-Müller-Schrader convergence theorem so that the Recognition Science framework can treat Regge calculus as a discrete precursor to general relativity. The local setting is that full formalization would require multi-year development of Riemannian geometry and functional analysis in Mathlib; the axioms are therefore labeled clearly for later replacement. Upstream imports supply auxiliary notions such as the smooth type from AczelProof and identity maps from VantageCategory, though these are not invoked by the list itself.
proof idea
The definition is realized as a direct list literal. No lemmas are applied and no tactics are used; the body simply constructs the List String value by enumeration of the five technical areas.
why it matters
The declaration documents the gap between the axiomatic treatment of Regge-to-GR convergence and a complete formal proof, justifying the use of axioms such as regge_to_eh_convergence inside the Recognition Science gravity module. It points to the 1984 Cheeger-Müller-Schrader result as the literature foundation. The entry touches the open question of when Mathlib will contain sufficient comparison geometry to discharge the axioms and render the RS gravity development fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.