---
id: F-030
title: Uniformly vanishing mean of the large-prime log tail
tier: lean
polarity: positive
depends_on: [F-029]
supersedes: []
verifier: export PATH="$HOME/.elan/bin:$PATH"; diff -u verified_math/F-030_vanishing-mean-log-tail/lean/Research/TailMean.lean workspace/experiments/experiment_3_adjacent_equal_density/lean/Research/TailMean.lean && (cd workspace/experiments/experiment_3_adjacent_equal_density/lean && lake build)
date: 2026-07-11
---

## Statement

For every `ε>0` there is a fixed prime cutoff `Z` such that, for every positive
`N`,

\[
 \sum_{m=1}^{N}\operatorname{tailLogLoss}(Z,m)<\varepsilon N.
\]

Formal theorem: `exists_uniform_mean_tailLogLoss_lt`.  The artifact also proves
the exact prime-by-prime rearrangement

\[
 \sum_{m=1}^{N}T_Z(m)=\sum_{Z<p\le N}\lfloor N/p\rfloor\,[-\log(1-1/p)].
\]

## Proof / verification

A prime `p` divides exactly `⌊N/p⌋` positive integers through `N`.  F-029
bounds its exact log weight by `1/(p-1)`, reducing the mean to the summable
kernel `1/(p(p-1))≤2/p²`.  The Cauchy tail criterion for the formally known
zeta-two series makes every finite high-prime kernel sum uniformly smaller
than `ε`, independently of `N`.

Artifact: `lean/Research/TailMean.lean`; Lean accepts it with no `sorry`,
`admit`, native evaluator axiom, or project-declared axiom.
