Gravity Analysis Quadrature Limit Sq Error Sum Tendsto Zero

The collapsing error sum

The classical fact behind this result is a standard piece of calculus: if you approximate an integral by a sum of many small pieces, the approximation gets better as the pieces get finer. The theorem sq_error_sum_tendsto_zero concerns the error terms in such an approximation. It proves that if each individual error term is bounded by a constant divided by the square of the number of pieces, then the total of all the absolute errors tends to zero as the number of pieces grows.

In plainer terms, imagine dividing a curved shape into N thin vertical strips. The error from each strip is small, but there are N of them, so the total error could in principle stay large. The theorem shows that if each strip's error shrinks like 1/N², then the sum of all N errors shrinks like 1/N, which goes to zero. This is a precise, machine-checked statement: the formal proof in the framework's library of theorems establishes that the sum of absolute errors tends to zero under exactly this condition.

This result is a tool, not a physical claim. It belongs to a toolkit for converting discrete sums over a lattice into continuous integrals, a bridge needed when a discrete model of gravity is taken to a continuum limit. The theorem itself says nothing about gravity, space, or any physical quantity. It is a statement about real numbers and limits, proved from the standard axioms of mathematics.

What the theorem does not claim is equally precise. It does not assert that any particular discrete gravity model converges to a continuum theory. It does not say that the error bound 1/N² actually holds for any physical system. It only states the conditional implication: if such a bound holds, then the total error vanishes in the limit. The question of whether the bound holds for a specific model is a separate, open matter.

/-- THEOREM (remainder collapse). If the per-term errors `g N k` are
uniformly bounded by `C/N²` for `k < N`, then the `N`-term absolute error
sum `Σ_{k<N} |g N k|` tends to `0`: the total error is at most `C/N`.
Load-bearing for Phase 4 remainder terms (curved perturbations of the flat
spectrum enter as `O(1/N²)` per mode). -/
theorem sq_error_sum_tendsto_zero (g : ℕ → ℕ → ℝ) (C : ℝ)
    (hg : ∀ N : ℕ, ∀ k, k < N → |g N k| ≤ C / (N : ℝ) ^ 2) :
    Filter.Tendsto (fun N : ℕ => ∑ k ∈ Finset.range N, |g N k|)
      Filter.atTop (nhds 0) := by
  have hub : ∀ N : ℕ, (∑ k ∈ Finset.range N, |g N k|) ≤ C / (N : ℝ) := by
    intro N
    calc (∑ k ∈ Finset.range N, |g N k|)
        ≤ ∑ _k ∈ Finset.range N, C / (N : ℝ) ^ 2 :=
          Finset.sum_le_sum fun k hk => hg N k (Finset.mem_range.1 hk)
      _ = (N : ℝ) * (C / (N : ℝ) ^ 2) := by
          rw [Finset.sum_const, Finset.card_range, nsmul_eq_mul]
      _ = C / (N : ℝ) := by
          rcases Nat.eq_zero_or_pos N with h0 | hpos
          · subst h0; simp
          · have hN0 : (N : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr hpos.ne'
            field_simp
  exact squeeze_zero (fun N => Finset.sum_nonneg fun k _ => abs_nonneg _) hub
    (tendsto_const_div_atTop_nhds_zero_nat C)

/-- THEOREM (remainder collapse). If the per-term errors `g N k` are
uniformly bounded by `C/N²` for `k < N`, then the `N`-term absolute error
sum `Σ_{k<N} |g N k|` tends to `0`: the total error is at most `C/N`.
Load-bearing for Phase 4 remainder terms (curved perturbations of the flat
spectrum enter as `O(1/N²)` per mode). -/
theorem sq_error_sum_tendsto_zero (g : ℕ → ℕ → ℝ) (C : ℝ)
    (hg : ∀ N : ℕ, ∀ k, k < N → |g N k| ≤ C / (N : ℝ) ^ 2) :
    Filter.Tendsto (fun N : ℕ => ∑ k ∈ Finset.range N, |g N k|)
      Filter.atTop (nhds 0) := by
  have hub : ∀ N : ℕ, (∑ k ∈ Finset.range N, |g N k|) ≤ C / (N : ℝ) := by
    intro N
    calc (∑ k ∈ Finset.range N, |g N k|)
        ≤ ∑ _k ∈ Finset.range N, C / (N : ℝ) ^ 2 :=
          Finset.sum_le_sum fun k hk => hg N k (Finset.mem_range.1 hk)
      _ = (N : ℝ) * (C / (N : ℝ) ^ 2) := by
          rw [Finset.sum_const, Finset.card_range, nsmul_eq_mul]
      _ = C / (N : ℝ) := by
          rcases Nat.eq_zero_or_pos N with h0 | hpos
          · subst h0; simp
          · have hN0 : (N : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr hpos.ne'
            field_simp
  exact squeeze_zero (fun N => Finset.sum_nonneg fun k _ => abs_nonneg _) hub
    (tendsto_const_div_atTop_nhds_zero_nat C)

What this page does not claim

This theorem does not prove that any discrete gravity model converges to a continuum theory. This theorem does not establish that the 1/N² error bound holds for any physical system. This theorem does not assign any physical meaning to the error terms themselves.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Gravity/Analysis/QuadratureLimit.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: