convergence_is_second_order

formal source

  95
  96/-- The convergence rate is second order: error = O(a^2).
  97    This means halving the mesh size quarters the error. -/
  98theorem convergence_is_second_order (a : ℝ) (ha : 0 < a) (ha1 : a < 1) :
  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 :=