rs_implies_gr
If the RSReggeConvergence structure holds, the Regge action on the J-cost lattice converges to the Einstein-Hilbert action with error bounded by kappa times a squared for mesh size a between zero and one. Discrete gravity researchers cite this to justify replacing the continuum Einstein-Hilbert action with its Regge counterpart inside the Recognition Science framework. The declaration is a direct definition that packages the second-order convergence statement as a proposition.
claimAssume the structure asserting Regge action convergence to the Einstein-Hilbert action at order $a^2$ together with the coupling relation $kappa_{RS}=8phi^5$. The defined statement asserts that for all real $a$ with $0<a<1$ there exists a real error such that $|error|leq kappa_{RS} a^2$.
background
The module axiomatizes the Cheeger-Müller-Schrader convergence theorem, which states that the Regge action on a refined simplicial approximation converges to the Einstein-Hilbert action at order O(a^2) in the mesh size. RSReggeConvergence is the structure containing the action convergence axiom, the Ricci convergence axiom, the derived coupling kappa_RS equal to eight phi to the fifth, and the positivity of kappa. This allows the Recognition Science lattice, whose dynamics follow from J-cost minimization, to reproduce the Einstein field equations via the variational principle on the converged action. The local setting imports Regge calculus definitions that supply the discrete curvature expressions used in the axioms.
proof idea
The declaration is a definition that directly encodes the quantified error bound as the body of the proposition. No lemmas are applied; it serves as an interface that assumes the convergence axioms from the referenced structure.
why it matters in Recognition Science
This definition bridges the discrete Regge calculus to the continuum general relativity within the Recognition Science framework. It enables derivation of the Einstein field equations from J-cost minimization on the lattice once the convergence axioms are granted. The module notes that a full proof would require simplicial geometry and comparison theorems not yet formalized in Mathlib, so the result remains an axiom package rather than a derived theorem. It touches the open question of formalizing Cheeger-Müller-Schrader in dependent type theory.
scope and limits
- Does not derive the convergence from the Recognition Science forcing chain or J-uniqueness.
- Does not provide an explicit bound on the constant in the error term beyond the kappa factor.
- Does not extend to non-vacuum spacetimes or include matter couplings.
- Does not guarantee convergence in the presence of singularities or topology changes.
formal statement (Lean)
128def rs_implies_gr (conv : RSReggeConvergence) : Prop :=
proof body
Definition body.
129 ∀ (a : ℝ), 0 < a → a < 1 →
130 ∃ (error : ℝ), |error| ≤ rs_kappa * a ^ 2
131
132/-! ## What Would Be Needed to Prove (Instead of Axiomatize) -/
133
134/-- To PROVE the convergence axioms from scratch in Lean, one would need:
135
136 1. Simplicial geometry: volumes, angles, areas as functions of edge lengths
137 (Cayley-Menger determinants, generalized to all dimensions)
138 2. The Schläfli identity: sum A_h * d(delta_h)/dL_e = 0
139 (a purely geometric identity; provable but technical)
140 3. Comparison geometry: relating simplicial metrics to smooth metrics
141 (this requires Riemannian geometry in Mathlib, which is incomplete)
142 4. Error analysis: bounding the difference between Regge curvature
143 and smooth curvature in terms of mesh quality
144 (the core of Cheeger-Müller-Schrader; very technical)
145 5. Compactness and convergence: extracting a convergent subsequence
146 and identifying the limit (standard but requires functional analysis)
147
148 This is a multi-year project for the Mathlib community.
149 We axiomatize instead, clearly labeling the axioms. -/