error_vanishes

formal source

  99    (a / 2) ^ 2 = a ^ 2 / 4 := by ring
 100
 101/-- Second-order convergence implies the error vanishes as a -> 0. -/
 102theorem error_vanishes (C : ℝ) (hC : 0 < C) :
 103    Filter.Tendsto (fun a => C * a ^ 2) (nhds 0) (nhds 0) := by
 104  have h : Continuous (fun a : ℝ => C * a ^ 2) := by continuity
 105  have := h.tendsto (0 : ℝ)
 106  simp at this
 107  exact this
 108
 109/-! ## Connection to RS -/
 110
 111/-- In the RS framework, the Regge action convergence gives:
 112    S_Regge(J-cost lattice, a) -> (1/2*kappa_RS) * integral R sqrt(g)
 113
 114    Combined with:
 115    - J-cost minimization implies delta S_Regge = 0 (variational dynamics)
 116    - delta S_EH = 0 implies EFE (Hilbert variation)
 117    - kappa_RS = 8*phi^5 (derived coupling)
 118
 119    This gives the FULL (nonlinear) Einstein field equations
 120    from the RS discrete ledger, conditional on the convergence axiom. -/
 121structure RSReggeConvergence where
 122  action_convergence : regge_to_eh_convergence_axiom
 123  ricci_convergence : regge_ricci_convergence_axiom
 124  kappa_derived : rs_kappa = 8 * phi ^ 5
 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) -/