Gravity Analysis Quadrature Limit Lattice Sum Tendsto Integral

The hinge-sum limit

The classical fact at the center of this result is elementary. Take a continuous function on the unit interval, sample it at N evenly spaced points, and average the samples. As N grows, that average approaches the integral of the function over the interval. This is the standard convergence of Riemann sums, a foundational result of calculus that Bernhard Riemann formalized in the 1850s. The theorem named latticeSum_tendsto_integral states precisely this: for any continuous real function f on [0, 1], the expression (1/N) Σ_{k

The proof is not new mathematics; it is a rigorous, machine-checked derivation of a known result. The framework's library, a machine-checked collection of formal theorems, proves it from scratch using Heine-Cantor uniform continuity and the splitting of the integral over adjacent intervals. This matters because the standard mathematical libraries lacked an elementary statement of this convergence for uniform meshes, working instead at the level of tagged partitions. The theorem fills that gap with a clean, axiom-clean proof, meaning it relies only on the standard axioms of the underlying logic, with no unproven assumptions.

In Recognition Science, this theorem acts as a bridge. The framework models discrete gravity as sums over lattice hinges, one summand per hinge. The expression (1/N) Σ f(k/N) is exactly the shape of those hinge sums, with spacing 1/N. The theorem proves that as the lattice refines, these discrete sums converge to the continuum integral. This is the mathematical justification for passing from a discrete model of gravity to a continuous one, a step the framework's later phases consume directly.

What the theorem does not claim is equally important. It does not assert that any particular physical quantity equals an integral; it only establishes convergence for continuous functions. It does not prove that the discrete gravity model itself is correct or that its hinge sums represent actual physics. The theorem is a tool, not a physical statement. It also does not address functions that are not continuous, where such convergence can fail. The result is a precise, limited mathematical fact, and its power lies in that precision.

/-- 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 (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 (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]

What this page does not claim

The theorem does not assert that any particular physical quantity equals an integral. The theorem does not prove that the discrete gravity model itself is physically correct. The theorem does not apply to discontinuous functions, where such convergence can fail.

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: