theorem
proved
tactic proof
error_vanishes
show as:
view Lean formalization →
formal statement (Lean)
102theorem error_vanishes (C : ℝ) (hC : 0 < C) :
103 Filter.Tendsto (fun a => C * a ^ 2) (nhds 0) (nhds 0) := by
proof body
Tactic-mode proof.
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. -/