IndisputableMonolith.Gravity.Analysis.QuadratureLimit
Analysis toolkit proving that uniform-mesh left Riemann sums, plain lattice sums, and weighted lattice sums of continuous functions on a compact interval converge to the corresponding integrals as mesh size goes to zero. Gravity continuum-limit arguments cite it when discrete Regge or hypersurface actions must pass to continuum integrals. Proofs rest on Heine-Cantor uniform continuity plus cell-by-cell error estimates.
claimFor $f:\mathbb{R}\to\mathbb{R}$ continuous on $[a,b]$ with $a\le b$, the left-endpoint Riemann sums $\sum_{k<N} f\bigl(a+k(b-a)/N\)\cdot(b-a)/N$ tend to $\int_a^b f$ as $N\to\infty$. Parallel statements hold for unweighted and weighted lattice sums, and the squared and absolute cell-error sums vanish in the continuum limit.
background
Recognition Science gravity continuum limits reduce discrete lattice actions (Regge, Freudenthal, hypersurface brackets) to continuum integrals. The analytic bottleneck is always the same: show that a mesh sum of a continuous density converges to an ordinary Riemann integral.
This module isolates that bottleneck. It works on a compact real interval $[a,b]$ with the standard uniform partition of width $(b-a)/N$. The core object is the left-endpoint Riemann sum; lattice and weighted-lattice variants rephrase the same sum in the language used by periodic $N$-site gravity models. Error sums (absolute and squared) quantify the residual between the discrete sum and the integral.
The setting is pure real analysis (Mathlib interval integrals and uniform continuity). No Recognition-specific constants appear here; the module is deliberately domain-agnostic so that 3D and 4D continuum-limit modules can import it without carrying gravity hypotheses.
proof idea
The core argument for the Riemann-sum limit uses Heine-Cantor: continuous $f$ on compact $[a,b]$ is uniformly continuous. Split the integral into $N$ adjacent mesh cells via the standard adjacent-interval sum lemma. On each cell the integrand differs from the left-endpoint sample by at most $\varepsilon$ once the mesh is finer than the uniform-continuity modulus $\delta$. Each cell therefore contributes an error at most $\varepsilon\cdot(b-a)/N$, and the total error is at most $\varepsilon(b-a)$.
Lattice and weighted-lattice statements are rephrasings of the same estimate (weights enter as bounded continuous multipliers). The absolute and squared error-sum lemmas package the residual for later $\ell^2$-style continuum arguments; both tend to zero by the same uniform-continuity bound.
why it matters in Recognition Science
Three gravity continuum modules import this file. Regge4DTorusContinuumLimit needs the quadrature limit to pass the finite periodic Freudenthal action on an $N^4$-site 4-torus (density weight $N^{-4}$) to its continuum symbol. DiracAlgebraContinuum lands the sampled-lapse Wronskian rate-$h$ residual as a continuum dynamic-bracket shape, relying on the weighted lattice sum limit. WeightedHypersurfaceBracket generalizes the frozen hypersurface-deformation bracket to a background weight $w$ on the periodic lattice and needs the weighted sum to converge.
Without a reusable, Mathlib-backed quadrature lemma, each of those continuum arguments would re-prove elementary real analysis in situ. The module therefore sits at the analysis base of the QG Seven-Gaps continuum campaign and the 4D Regge torus path, parallel to the closed 3D route through ReggeTTContinuumLimit.
scope and limits
- Does not treat non-uniform meshes, adaptive partitions, or higher-order quadrature rules.
- Does not address discontinuous or merely integrable densities; continuity on a compact interval is required.
- Does not encode gravity, curvature, or Recognition constants; pure real-analysis statements only.
- Does not prove multi-dimensional product integrals; callers must tensor or iterate the 1D result.
- Does not supply rates of convergence beyond the uniform-continuity modulus argument.