---
id: F-033
title: Equal adjacent totients have upper density below one third
tier: lean
polarity: negative
depends_on: [F-029, F-030, F-032]
supersedes: []
verifier: export PATH="$HOME/.elan/bin:$PATH"; diff -u verified_math/F-033_adjacent-equal-upper-density/lean/Research/AdjacentEqualUpper.lean workspace/experiments/experiment_3_adjacent_equal_density/lean/Research/AdjacentEqualUpper.lean && (cd workspace/experiments/experiment_3_adjacent_equal_density/lean && lake build)
date: 2026-07-11
---

## Statement

Under the positive-integer convention,

```lean
∀ᶠ N : ℕ in atTop,
  (Nat.count SuccessorTotientEqual N : ℝ) < (N : ℝ) / 4.
```

After shifting to the starts used in the weak-pattern formalization, this gives

```lean
∀ᶠ N : ℕ in atTop,
  (Nat.count AdjacentTotientEqual N : ℝ) < (N : ℝ) / 3.
```

Consequently, because equality, increase, and decrease partition all adjacent
pairs, equality cannot eventually dominate both strict orders.  Formal
results are `eventually_successorTotientEqual_count_lt_quarter`,
`eventually_adjacentTotientEqual_count_lt_third`, and
`equality_not_dominate_both_of_lt_third`.

## Proof / verification

Equal totients force the full logarithmic-loss difference to equal
`log(n+1)-log n`.  Outside a fixed initial range, if both large-prime tails are
small, the finite-prime difference lies in F-032's short interval.  F-030 and
finite Markov inequalities make each exceptional large-tail set have density
below `3/250`; F-032 bounds the concentrated set eventually by `1/5`.  Including
the fixed initial range gives the stated strict `1/4` bound.  A direct
three-way trichotomy then yields the strict-order consequence.

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