Curvature and Kernel Structure in Sum–Integral Comparison: II. Non-Uniform Partitions and Scaled Bounds

Curvature Theory Lean Formalisation This repository contains a Lean 4 formalisation of the results in the paper: “Curvature and Kernel Structure in Sum–Integral Comparison: II. Non-Uniform Partitions and Scaled Bounds” Overview This project develops a fully formal, inequality-based framework for sum–integral comparison over non-uniform partitions, based on a curvature (kernel) representation of the trapezoidal error. The central identity is: trapezoidDefect(f, a, b) = (1/2) ∫ₐᵇ (x − a)(b − x) f''(x) dx This expresses the trapezoidal error on an interval as a weighted integral of the second derivative, with kernel (x − a)(b − x). From this identity, the formalisation derives sharp local bounds of the form: D(f; a, b) ≈ ((b − a)³ / 12) · f''(·) showing that the error scales cubically with the interval length. These local estimates are then assembled over arbitrary partitions to obtain a global non-uniform quadrature theorem: R(f; 𝓟) = ∑ᵢ D(f; xᵢ, xᵢ₊₁) with bounds: ∑ᵢ ((xᵢ₊₁ − xᵢ)³ / 12) · mᵢ ≤ R(f; 𝓟) ≤ ∑ᵢ ((xᵢ₊₁ − xᵢ)³ / 12) · Mᵢ Formalisation All results are fully formalised and verified in Lean 4. The development is deliberately minimal and structured into six files: Defs.lean — basic definitions (trapezoid defect, partitions, remainder) SmoothKernel.lean — kernel identity via integration by parts ScaledKernel.lean — scaled kernel identity on general intervals ScaledBounds.lean — local curvature bounds with cubic scaling NonUniformSum.lean — partition sums and additivity NonUniformComparison.lean — global non-uniform quadrature theorem The entire development can be imported via: import CurvatureTheory Mathematical Contribution The formalisation provides a curvature-based framework for sum–integral comparison that: yields exact non-asymptotic bounds applies to arbitrary non-uniform partitions makes the cubic dependence on mesh size explicit avoids classical Euler–Maclaurin expansions and Bernoulli numbers The approach highlights a geometric interpretation of quadrature error in terms of curvature and local interval structure. Reproducibility The project builds using: Lean 4 (v4.29.0-rc4) Mathlib (matching version) lake build All proofs are explicit and designed to be robust and auditable. Documentation docs/paper.pdf — accompanying research paper docs/lean-to-paper.md — mapping between the Lean formalisation and the paper Author Bob JeffersonORCID: 0009-0003-1460-055X Citation If you use this work, please cite the accompanying paper and this Zenodo record.