Encyclopedia Gravity Gravity Analysis Quadrature Limit

ARTICLE 4 claims 4 theorems

Gravity Analysis Quadrature Limit

A machine-checked proof that discrete sums over a lattice converge to continuous integrals, a bridge between discrete gravity and continuum physics.

Verify this page

Quadrature limit

In numerical analysis, a quadrature rule approximates a definite integral by a weighted sum of function values at discrete points. The simplest such rule is the left-endpoint Riemann sum: divide an interval into N equal pieces, evaluate the function at each piece's left edge, multiply by the piece width, and add. The classical theorem states that for a continuous function on a closed interval, these sums converge to the integral as N grows without bound.

The module QuadratureLimit in the framework's machine-checked library of formal theorems proves this convergence from scratch, without relying on pre-packaged results. Its core lemma, riemannSum_tendsto_integral, states that for any continuous function f on [a, b], the left-endpoint uniform-mesh sums converge to the integral of f over that interval. The proof uses uniform continuity, which follows from compactness of the interval, and splits the integral into N adjacent pieces to bound each cell's error.

Beyond the basic result, the module proves three specialized forms that matter for discrete gravity. The lattice sum form, latticeSum_tendsto_integral, handles averages over points k/N in [0,1], converging to the integral of f. The weighted form, weightedLatticeSum_tendsto, includes a continuous weight function w, so the sum of f(k/N)w(k/N)/N converges to the integral of f times w. Finally, two remainder-collapse lemmas show that if per-term errors are bounded by C/N², then the total error over N terms vanishes as N grows.

In Recognition Science, these lemmas build a bridge from discrete lattice models to continuum physics. The lattice sums represent sums over hinge points in a discrete spacetime, and the limit theorems show that as the lattice spacing shrinks, these sums approach ordinary integrals. This matters for the framework's gravity campaign, where Phase 4 uses the remainder estimates to handle curved perturbations of flat spectra, and Phase 5 uses the weighted sums to pass from discrete actions to continuum integrals.

The practical consequence is that discrete models of gravity can be analyzed with continuum tools, provided the functions involved are continuous. The proofs are axiom-clean, meaning they rely only on the standard postulates of the ambient type theory, with no framework-specific axioms. This gives the bridge a firm logical footing: the limit is not assumed, but derived.

THEOREM riemannSum_tendsto_integral · IndisputableMonolith/Gravity/Analysis/QuadratureLimit.lean
riemannSum_tendsto_integral · IndisputableMonolith/Gravity/Analysis/QuadratureLimit.lean:54 
/-- THEOREM (core quadrature limit). For `f : ℝ → ℝ` continuous on `[a, b]`
with `a ≤ b`, the left-endpoint uniform-mesh Riemann sums
`Σ_{k<N} f(a + k(b-a)/N) · ((b-a)/N)` converge to `∫ x in a..b, f x` as
`N → ∞`.

Proof: Heine-Cantor gives uniform continuity of `f` on the compact interval;
splitting the integral over the `N` mesh cells
(`intervalIntegral.sum_integral_adjacent_intervals`) reduces the error to a
sum of `N` cell errors, each bounded by `ε · (b-a)/N` once the mesh
`(b-a)/N` is below the uniform-continuity scale `δ`. -/
theorem riemannSum_tendsto_integral (f : ℝ → ℝ) (a b : ℝ) (hab : a ≤ b)
    (hf : ContinuousOn f (Set.Icc a b)) :
    Filter.Tendsto
      (fun N : ℕ => ∑ k ∈ Finset.range N,
        f (a + (k : ℝ) * (b - a) / (N : ℝ)) * ((b - a) / (N : ℝ)))
      Filter.atTop (nhds (∫ x in a..b, f x)) := by
  rcases eq_or_lt_of_le hab with heq | hlt
  · subst heq
    simp only [sub_self, mul_zero, zero_div, add_zero,
      Finset.sum_const_zero, intervalIntegral.integral_same]
    exact tendsto_const_nhds
  · have hba : 0 < b - a := sub_pos.2 hlt
    rw [Metric.tendsto_atTop]
    intro ε hε
    set ε' : ℝ := ε / (2 * (b - a)) with hε'def
    have hε' : 0 < ε' := div_pos hε (by linarith)
    obtain ⟨δ, hδpos, hδ⟩ :=
      Metric.uniformContinuousOn_iff_le.1
        (isCompact_Icc.uniformContinuousOn_of_continuous hf) ε' hε'
    obtain ⟨M, hM⟩ := exists_nat_ge ((b - a) / δ)
    refine ⟨max M 1, fun N hN => ?_⟩
    have hN1 : 1 ≤ N := le_trans (le_max_right M 1) hN
    have hNM : M ≤ N := le_trans (le_max_left M 1) hN
    have hNpos : (0 : ℝ) < (N : ℝ) := by exact_mod_cast Nat.lt_of_lt_of_le Nat.zero_lt_one hN1
    have hN0 : (N : ℝ) ≠ 0 := ne_of_gt hNpos
    have hmesh : (b - a) / (N : ℝ) ≤ δ := by
      rw [div_le_iff₀ hNpos]
      have h1 : (b - a) / δ ≤ (N : ℝ) := le_trans hM (by exact_mod_cast hNM)
      have h2 : δ * ((b - a) / δ) ≤ δ * (N : ℝ) :=
        mul_le_mul_of_nonneg_left h1 hδpos.le
      have h3 : δ * ((b - a) / δ) = b - a := by field_simp
      linarith
    set p : ℕ → ℝ := fun k => a + (k : ℝ) * (b - a) / (N : ℝ) with hp
    have hp0 : p 0 = a := by simp [hp]
    have hpN : p N = b := by
      simp only [hp]
      field_simp
      ring
    have hstep : ∀ k : ℕ, p (k + 1) - p k = (b - a) / (N : ℝ) := by
      intro k
      simp only [hp]
      push_cast
      ring
    have hmeshpos : 0 ≤ (b - a) / (N : ℝ) := div_nonneg hba.le hNpos.le
    have hple : ∀ k : ℕ, p k ≤ p (k + 1) := by
      intro k
      have := hstep k
      linarith
    have hmem : ∀ k : ℕ, k ≤ N → p k ∈ Set.Icc a b := by
      intro k hk
      have hkN : (k : ℝ) ≤ (N : ℝ) := by exact_mod_cast hk
      have hq : 0 ≤ (b - a) / (N : ℝ) := hmeshpos
      have h2 := mul_le_mul_of_nonneg_left hkN hq
      have hNb : (b - a) / (N : ℝ) * (N : ℝ) = b - a := by field_simp
      have hknn : 0 ≤ (k : ℝ) * (b - a) / (N : ℝ) :=
        div_nonneg (mul_nonneg (Nat.cast_nonneg k) hba.le) hNpos.le
      have hcomm : (k : ℝ) * (b - a) / (N : ℝ) = (b - a) / (N : ℝ) * (k : ℝ) := by
        ring
      constructor
      · simp only [hp]
        linarith
      · simp only [hp]
        linarith [h2, hNb, hcomm]
    have hint : ∀ k, k < N → IntervalIntegrable f volume (p k) (p (k + 1)) := by
      intro k hk
      apply ContinuousOn.intervalIntegrable
      apply hf.mono
      rw [Set.uIcc_of_le (hple k)]
      exact Set.Icc_subset_Icc (hmem k hk.le).1 (hmem (k + 1) hk).2
    have hsplit : (∑ k ∈ Finset.range N, ∫ x in p k..p (k + 1), f x)
        = ∫ x in a..b, f x := by
      rw [intervalIntegral.sum_integral_adjacent_intervals hint, hp0, hpN]
    have hkey : (∑ k ∈ Finset.range N, f (p k) * ((b - a) / (N : ℝ)))
        - (∫ x in a..b, f x)
        = ∑ k ∈ Finset.range N, ∫ x in p k..p (k + 1), (f (p k) - f x) := by
      rw [← hsplit, ← Finset.sum_sub_distrib]
      refine Finset.sum_congr rfl fun k hk => ?_
      have hk' : k < N := Finset.mem_range.1 hk
      have hsub : (∫ x in p k..p (k + 1), (f (p k) - f x))
          = (∫ _x in p k..p (k + 1), f (p k)) - ∫ x in p k..p (k + 1), f x :=
        intervalIntegral.integral_sub intervalIntegrable_const (hint k hk')
      rw [hsub, intervalIntegral.integral_const, hstep k, smul_eq_mul]
      ring
    have hbound : ∀ k ∈ Finset.range N,
        |∫ x in p k..p (k + 1), (f (p k) - f x)| ≤ ε' * ((b - a) / (N : ℝ)) := by
      intro k hk
      have hk' : k < N := Finset.mem_range.1 hk
      have hCbound : ∀ x ∈ Set.uIoc (p k) (p (k + 1)), ‖f (p k) - f x‖ ≤ ε' := by
        intro x hx
        rw [Set.uIoc_of_le (hple k)] at hx
        have hxmem : x ∈ Set.Icc a b :=
          ⟨le_trans (hmem k hk'.le).1 hx.1.le, le_trans hx.2 (hmem (k + 1) hk').2⟩
        have hdist : dist (p k) x ≤ δ := by
          rw [Real.dist_eq, abs_of_nonpos (by linarith [hx.1.le] : p k - x ≤ 0)]
          have hupper : x ≤ p k + (b - a) / (N : ℝ) := by
            have := hstep k
            linarith [hx.2]
          linarith [hmesh]
        have h := hδ (p k) (hmem k hk'.le) x hxmem hdist
        rw [Real.dist_eq] at h
        rwa [Real.norm_eq_abs]
      calc |∫ x in p k..p (k + 1), (f (p k) - f x)|
          ≤ ε' * |p (k + 1) - p k| := by
            rw [← Real.norm_eq_abs]
            exact intervalIntegral.norm_integral_le_of_norm_le_const hCbound
        _ = ε' * ((b - a) / (N : ℝ)) := by
            rw [hstep k, abs_of_nonneg hmeshpos]
    have hsum_bound : |(∑ k ∈ Finset.range N, f (p k) * ((b - a) / (N : ℝ)))
        - ∫ x in a..b, f x| ≤ ε' * (b - a) := by
      rw [hkey]
      calc |∑ k ∈ Finset.range N, ∫ x in p k..p (k + 1), (f (p k) - f x)|
          ≤ ∑ k ∈ Finset.range N, |∫ x in p k..p (k + 1), (f (p k) - f x)| :=
            Finset.abs_sum_le_sum_abs _ _
        _ ≤ ∑ _k ∈ Finset.range N, ε' * ((b - a) / (N : ℝ)) :=
            Finset.sum_le_sum hbound
        _ = (N : ℝ) * (ε' * ((b - a) / (N : ℝ))) := by
            rw [Finset.sum_const, Finset.card_range, nsmul_eq_mul]
        _ = ε' * (b - a) := by
            field_simp
    have hfinal : ε' * (b - a) < ε := by
      have hhalf : ε' * (b - a) = ε / 2 := by
        rw [hε'def]
        field_simp
      linarith [hhalf]
    rw [Real.dist_eq]
    exact lt_of_le_of_lt hsum_bound hfinal
THEOREM latticeSum_tendsto_integral · IndisputableMonolith/Gravity/Analysis/QuadratureLimit.lean
latticeSum_tendsto_integral · IndisputableMonolith/Gravity/Analysis/QuadratureLimit.lean:191 
/-- THEOREM (campaign-facing hinge-sum form). For `f` continuous on `[0, 1]`,
the lattice averages `(1/N) Σ_{k<N} f(k/N)` converge to `∫ x in 0..1, f x`.
This is the exact shape of discrete-gravity hinge sums (one summand per
lattice hinge, spacing `1/N`); Phases 4 and 5 consume it directly. -/
theorem latticeSum_tendsto_integral (f : ℝ → ℝ)
    (hf : ContinuousOn f (Set.Icc 0 1)) :
    Filter.Tendsto
      (fun N : ℕ => (1 / (N : ℝ)) * ∑ k ∈ Finset.range N, f ((k : ℝ) / (N : ℝ)))
      Filter.atTop (nhds (∫ x in (0:ℝ)..1, f x)) := by
  have h := riemannSum_tendsto_integral f 0 1 zero_le_one hf
  refine h.congr fun N => ?_
  rw [Finset.mul_sum]
  refine Finset.sum_congr rfl fun k _ => ?_
  have harg : (0 : ℝ) + (k : ℝ) * (1 - 0) / (N : ℝ) = (k : ℝ) / (N : ℝ) := by ring
  have hw : ((1 : ℝ) - 0) / (N : ℝ) = 1 / (N : ℝ) := by norm_num
  rw [harg, hw, mul_comm]
THEOREM weightedLatticeSum_tendsto · IndisputableMonolith/Gravity/Analysis/QuadratureLimit.lean
weightedLatticeSum_tendsto · IndisputableMonolith/Gravity/Analysis/QuadratureLimit.lean:208 
/-- THEOREM (weighted hinge-sum form). For `f` and a weight `w` both
continuous on `[0, 1]`, `(1/N) Σ_{k<N} f(k/N) w(k/N) → ∫ x in 0..1, f x · w x`.
A direct corollary of `latticeSum_tendsto_integral` applied to `f·w`; stated
separately because Phase 5 consumes exactly this weighted shape
(measure-weighted hinge sums). -/
theorem weightedLatticeSum_tendsto (f w : ℝ → ℝ)
    (hf : ContinuousOn f (Set.Icc 0 1)) (hw : ContinuousOn w (Set.Icc 0 1)) :
    Filter.Tendsto
      (fun N : ℕ => (1 / (N : ℝ)) *
        ∑ k ∈ Finset.range N, f ((k : ℝ) / (N : ℝ)) * w ((k : ℝ) / (N : ℝ)))
      Filter.atTop (nhds (∫ x in (0:ℝ)..1, f x * w x)) :=
  latticeSum_tendsto_integral (fun x => f x * w x) (hf.mul hw)
THEOREM sq_error_sum_tendsto_zero · IndisputableMonolith/Gravity/Analysis/QuadratureLimit.lean
sq_error_sum_tendsto_zero · IndisputableMonolith/Gravity/Analysis/QuadratureLimit.lean:221 
/-- 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

The module does not prove that all discrete gravity models converge to the same continuum limit, only that the sums in question converge for continuous integrands. This module does not establish the physical interpretation of the lattice spacing or the discrete action itself. The theorems do not apply to discontinuous functions or functions with unbounded variation.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND