---
id: F-032
title: One-sixth concentration bound for finite-prime adjacent loss
tier: lean
polarity: positive
depends_on: [F-031]
supersedes: []
verifier: export PATH="$HOME/.elan/bin:$PATH"; diff -u verified_math/F-032_finite-prime-one-sixth-concentration/lean/Research/Concentration.lean workspace/experiments/experiment_3_adjacent_equal_density/lean/Research/Concentration.lean && (cd workspace/experiments/experiment_3_adjacent_equal_density/lean && lake build)
date: 2026-07-11
---

## Statement

Let `D_Z(n)` be the adjacent difference of the exact logarithmic loss from
primes at most `Z`, and let `M_Z` be the product of primes in `(3,Z]`.  There is
a fixed constant `baseLogDiffGap>0` such that, for every `Z≥3`, center `c`, and
cutoff `N`,

```lean
Nat.count (fun n => |D_Z n - c| < baseLogDiffGap / 3) N ≤
  (N / (6 * M_Z) + 1) * M_Z.
```

In particular, at most `M_Z` of the `6M_Z` residues in a complete period lie
in any such interval.  Formal theorems are
`card_fixedLogDiff_close_one_period` and `count_fixedLogDiff_close_le`.

## Proof / verification

The six cutoff-three adjacent losses form a finite real set with positive
minimum separation and are injective on residues modulo six (F-031).  If two
qualifying residues agree modulo the coprime extra-prime modulus, periodicity
makes their extra contribution equal; the separation then makes their residues
modulo six equal.  The Chinese-remainder congruence and range bounds make the
map to the extra residue injective, giving the one-period cardinality bound.
A kernel-proved periodic-count induction extends this to every initial range,
with one incomplete-period error.

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