Gravity Analysis Quadrature Limit Weighted Lattice Sum Tendsto

The weighted hinge sum

A Riemann sum is a standard way to approximate the area under a curve: slice the region into thin rectangles, add their areas, and let the slices grow thinner. The classical result, taught in every calculus course, is that for a continuous function these sums converge to the definite integral as the mesh size goes to zero. The Recognition Science library proves this from scratch in a machine-checked collection of formal theorems, rather than importing it as a black box, because its discrete gravity program needs the statement in a specific weighted form.

The declaration weightedLatticeSum_tendsto establishes the weighted version. For two continuous functions f and w on the unit interval, the average of f(k/N) times w(k/N) over the N points k/N converges to the integral of the product f(x)w(x) as N goes to infinity. In symbols: (1/N) Σ f(k/N) w(k/N) → ∫ f(x) w(x) dx. This is a direct corollary of the unweighted lattice sum theorem applied to the product function, and it is proved, axiom-clean, with no gaps.

The name reflects its purpose in the framework's gravity campaign. A lattice is a discrete grid of points, and a hinge sum is a sum over the connections or hinges of that grid. The theorem says that when the grid spacing shrinks, these discrete hinge sums, weighted by some continuous factor, behave like ordinary integrals over the continuum. This is the bridge that lets discrete lattice calculations approximate smooth spacetime quantities in the limit of fine spacing.

What the theorem does not claim is just as important. It does not say that any particular discrete gravity theory is correct, nor that the continuum limit of a specific physical model exists. It is a pure analysis result: a statement about convergence of sums to integrals under continuity assumptions. It provides the analytical tool, not the physical conclusion. The theorem also requires both f and w to be continuous on the closed interval; it says nothing about discontinuous functions or about convergence rates, only that the limit exists.

/-- 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 (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 establish that any particular discrete gravity theory is physically correct. The theorem does not claim convergence for discontinuous functions or provide a convergence rate. The theorem does not assert that the continuum limit of a specific physical model exists.

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: