rs_implies_gr

formal source

 125  kappa_positive : 0 < rs_kappa
 126
 127/-- If the convergence axioms hold, then the RS lattice produces GR. -/
 128def rs_implies_gr (conv : RSReggeConvergence) : Prop :=
 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. -/
 150def proof_requirements : List String :=
 151  [ "Simplicial geometry (Cayley-Menger)"
 152  , "Schläfli identity"
 153  , "Comparison geometry (smooth vs piecewise-flat)"
 154  , "Curvature error analysis"
 155  , "Compactness and convergence extraction" ]
 156
 157/-! ## Certificate -/
 158