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. -/
depends on (29)
Lean names referenced from this declaration's body.