Curvature and Kernel Structure in Sum–Integral Comparison III: Asymptotic Equivalence under Mesh Refinement

This upload contains the paper and Lean 4 formalisation for: Curvature and Kernel Structure in Sum–Integral Comparison III: Asymptotic Equivalence under Mesh Refinement This is the third part of a series developing a curvature-based approach to sum–integral comparison. Part I established the kernel identity for the trapezoidal defect.Part II extended the theory to non-uniform partitions and scaled cubic-weight bounds.Part III completes the asymptotic layer of the theory. Main contributions of this part: - asymptotic equivalence of lower and upper cubic-weight comparison sums under mesh refinement- a clear separation between additive asymptotic equivalence and multiplicative ratio asymptotics- strengthened ratio results under additional comparability hypotheses- full Lean 4 formalisation of the mathematical development The viewpoint is complementary to classical Euler–Maclaurin analysis, but proceeds through curvature kernels, cellwise defect identities, and partition-based comparison estimates rather than Bernoulli-number expansions. The repository includes:- the LaTeX source of the paper- the Lean 4 source files- project documentation and citation metadata Relationship to prior work:This record should be linked as “Is supplement to” Part I of the series.