59 ∀ (S_EH : ℝ) (a : ℝ), 0 < a → a < 1 → 60 ∃ (S_Regge : ℝ) (C : ℝ), 0 < C ∧ 61 |S_Regge - S_EH| ≤ C * a ^ 2 62 63/-- **AXIOM (Regge Ricci convergence)**: 64 The Regge curvature (sum of deficit angles / dual volumes) 65 converges to the Ricci scalar at O(a^2). 66 67 For a smooth metric g at point x: 68 |R_Regge(x, a) - R(x)| <= C * a^2 69 70 This follows from the action convergence by the fundamental 71 theorem of calculus of variations. -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.