Curvature and Kernel Structure for Sum–Integral Comparison

This repository contains the complete materials for the paper: “Curvature and Kernel Structure in Sum–Integral Comparison”Bob Jefferson (2026) It includes: the full LaTeX source of the paper a fully verified Lean 4 formalisation of all main results supporting documentation and engineering logs Overview The paper develops an inequality-based framework for sum–integral comparison in which the remainder is controlled directly by curvature. Instead of relying on the classical Euler–Maclaurin expansion, the approach is based on: an exact decomposition into unit-scale trapezoid defects a kernel identity expressing each defect as an integral against a positive quadratic kernel monotonicity of the second derivative to obtain sharp bounds This yields a two-sided estimate of the form 112∑k≥N+1f′′ (k) ≤ RN (f) ≤ 112∑k≥Nf′′ (k), 112₊ ₍+₁ f'' (k) \;\; RN (f) \;\; 112₊ ₍ f'' (k), 121k≥N+1∑f′′ (k) ≤RN (f) ≤121k≥N∑f′′ (k), showing that the sum–integral discrepancy is governed directly by the discrete tail of the curvature. Key Features Exact structural decomposition of the remainder into local contributions Positive kernel representation of each trapezoid defect Sharp constant 1/121/121/12 arising geometrically from the kernel Two-sided global bounds under minimal monotonicity assumptions Explicit applications, including: ppp-series remainder estimates nonasymptotic Stirling-type bounds with uniform error control Fully formalised in Lean 4, ensuring complete verification Lean Formalisation All main results in the paper are formally verified in Lean 4 using mathlib. The formalisation includes: trapezoid decomposition of the remainder curvature kernel identity local and global curvature bounds specialisations to harmonic and ppp-series cases A detailed mapping between the paper and the Lean modules is provided in: LeanToPaperMap. md This ensures that every major theorem in the paper corresponds to a verified formal result. Repository Structure docs/ — paper source and supporting materials InequalityEM/ — Lean 4 formalisation engineering/ — module-by-module development logs LeanToPaperMap. md — mapping between paper and code Significance This work provides a structurally transparent alternative to the Euler–Maclaurin formula. Rather than relying on asymptotic expansions and Bernoulli numbers, the method: uses positivity and monotonicity instead of cancellation yields explicit, nonasymptotic bounds isolates curvature as the governing mechanism for the remainder The framework is particularly well suited to formal verification and robust quantitative estimates. Author Bob JeffersonORCID: 0009-0003-1460-055X License MIT License (see LICENSE) Citation Please cite using the metadata in CITATION. cff.