theorem
proved
term proof
latticeSpacing_tendsto_zero
show as:
view Lean formalization →
formal statement (Lean)
62theorem latticeSpacing_tendsto_zero (L : ℝ) (_hL : 0 < L) :
63 ∀ ε > 0, ∃ N₀ : ℕ, 0 < N₀ ∧ ∀ N : ℕ, N₀ ≤ N → latticeSpacing L N < ε := by
proof body
Term-mode proof.
64 intro ε hε
65 obtain ⟨N₀, hN₀⟩ := exists_nat_gt (L / ε)
66 refine ⟨N₀ + 1, Nat.succ_pos _, fun N hN => ?_⟩
67 unfold latticeSpacing
68 have hN_pos : (0 : ℝ) < (N : ℝ) := Nat.cast_pos.mpr (by omega)
69 rw [div_lt_iff₀ hN_pos]
70 have hN₀_le : (N₀ : ℝ) ≤ (N : ℝ) := Nat.cast_le.mpr (by omega)
71 nlinarith [div_lt_iff₀ hε |>.mp hN₀]
72
73/-! ## §2 Flat Spacetime Chain -/
74
75/-- The flat-spacetime chain: from J-cost through Minkowski to vanishing Einstein.
76
77 J(1+ε) = ε²/2 + O(ε⁴) → spatial metric g_ij = δ_ij →
78 η = diag(-1,+1,+1,+1) → Γ = 0 → R^ρ_σμν = 0 →
79 R_μν = 0 → R = 0 → G_μν = 0 -/