regge_riemann_convergence_axiom
plain-language theorem explainer
The declaration axiomatizes that holonomy around a plaquette of mesh size a converges to a Riemann curvature component at order a² with remainder O(a⁴). Researchers formalizing discrete gravity or citing Cheeger-Müller-Schrader would invoke it to justify passage from Regge calculus to continuum curvature. It is introduced as a direct Prop definition that encodes the error bound without internal derivation.
Claim. For any real component $R$ of the Riemann curvature tensor and mesh size satisfying $0 < a < 1$, there exist a holonomy deviation $h$ and constant $C > 0$ such that $|h - a^2 R| ≤ C a^4$.
background
The definition sits inside the NonlinearConvergence module, which axiomatizes the Cheeger-Müller-Schrader (1984) result that Regge actions on refined triangulations converge to the Einstein-Hilbert action at second order in mesh size. The module imports ReggeCalculus for simplicial structures and Constants for RS-native units. Upstream 'is' predicates from SimplicialLedger.EdgeLengthFromPsi and OptionAEmpiricalProgram supply collision-free edge lengths and empirical-program constraints that underwrite the discrete geometry.
proof idea
The declaration is a direct definition of the convergence statement as a universal quantifier over curvature component and mesh size a. No lemmas are invoked; the body simply asserts the existence of holonomy deviation and error constant C satisfying the stated O(a⁴) bound.
why it matters
The axiom supplies the Riemann-level convergence step required by the parent result rs_implies_gr, allowing the Regge action to recover the Einstein equations once the O(a²) limit is taken. It fills the geometric content of the deficit-angle-to-sectional-curvature map inside the gravity domain and references the Cheeger-Müller-Schrader theorem cited in the module doc-comment. It leaves open the question of replacing the axiom by a full Mathlib formalization of the 1984 convergence proof.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.