regge_ricci_convergence_axiom
plain-language theorem explainer
regge_ricci_convergence_axiom encodes the O(a²) convergence of the Regge curvature scalar to the continuum Ricci scalar for smooth metrics. A researcher passing from simplicial Regge calculus to the Einstein-Hilbert action would cite it to justify the continuum limit in discrete gravity models. The definition directly states that for any continuum curvature value and mesh size a in (0,1) there exist a Regge curvature and positive C satisfying the quadratic error bound.
Claim. For any continuum Ricci scalar $R_continuum$ and mesh size $a$ with $0 < a < 1$, there exist $R_Regge$ and $C > 0$ such that $|R_Regge - R_continuum| ≤ C a^2$.
background
The module axiomatizes the Cheeger-Müller-Schrader (1984) theorem that the Regge action on refined triangulations converges to the Einstein-Hilbert action at second order in mesh size. Regge curvature is the sum of deficit angles divided by dual volumes; the axiom isolates the induced scalar convergence, which follows from action convergence by the calculus of variations. The local setting is the limit of piecewise-flat geometries to smooth Riemannian metrics under refinement, with smoothness drawn from Cost.AczelTheorem.smooth (set to ∞).
proof idea
The declaration is a direct definition of the Prop. The body unfolds the universal quantifiers over R_continuum and a, then the existential for R_Regge and C with the stated bound. No lemmas or tactics are applied.
why it matters
It supplies the ricci_convergence field inside the RSReggeConvergence structure, which combines it with action convergence and kappa_RS = 8 phi^5 to recover the Einstein equations from J-cost minimization. This places the axiom at the Regge-to-GR interface in the Recognition framework, consistent with the forcing chain through T8 (D=3) and the variational principle. It leaves open replacement by a full Mathlib formalization of the 1984 result.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.