Cancellation in the actual harmonic tail
Abstract
Cancellation in the actual harmonic tail.
The arithmetic suppliers preserve the Terence Tao / Apache-2.0 attribution at LogConvolutionMassExpansion. Harmonic, Stirling, Abel and integral APIs are reused from pinned Mathlib. These are repository deductions, with no literature novelty claim. The literal factorial G is distinct from prime-weighted primitives in other RH routes.
Theorem 1.1 (A quadratic tail bound from genuine cancellation).
Lean statement: D5/S3/Arith/Robin/ActualContinuousFactorialCompensation/SharpTail/Cancellation.T_epsilon_quadratic_bound
Proof. Machine-checked in Lean as D5/S3/Arith/Robin/ActualContinuousFactorialCompensation/SharpTail/Cancellation.T_epsilon_quadratic_bound (✓ std3). ∎
Source. Repository-derived.
Commentary.
For every real x>=1, abs(T_epsilon(x))<=8/x^2. Abel summation identifies the integral of (1/2-fract(t))/t^2 with -harmonicPrimitive(x)/x. The remaining density is bounded using abs(harmonicPrimitive(t))<=4/t. The estimate is for the original improper integral, with no assumed decay hypothesis.