---
id: F-027
title: Eventual natural-frequency dominance implies Erdős #1003
tier: lean
polarity: positive
depends_on: [F-026]
supersedes: []
verifier: export PATH="$HOME/.elan/bin:$PATH"; diff -u verified_math/F-027_natural-frequency-implies-problem1003/lean/Research/WeakAmbiguity.lean workspace/experiments/experiment_1_formalize_patterns/lean/Research/WeakAmbiguity.lean && (cd workspace/experiments/experiment_1_formalize_patterns/lean && lake build)
date: 2026-07-11
---

## Statement

Give “most likely” the canonical cumulative uniform-start interpretation at
length two.  If, for all sufficiently large cutoffs, the natural equality
pattern occurs at least as often as the increasing pattern, then there are
infinitely many `n` satisfying

\[
  \phi(n)=\phi(n+1).
\]

Formal theorem:

```lean
theorem eventualNaturalDominance_implies_problem1003
    (h : EventuallyNaturalDominatesIncreasing) :
    Set.Infinite {n : ℕ | Nat.totient n = Nat.totient (n + 1)}
```

The artifact also proves unconditionally that increasing adjacent pairs occur
infinitely often.

## Proof / verification

For every sufficiently large prime `p`,
`φ(p-1)<p-1=φ(p)`, so increasing adjacent starts form an infinite set.  An
abstract kernel-checked counting lemma proves that if the cumulative count of
an infinite predicate is eventually bounded by a second cumulative count, then
the second predicate is infinite; otherwise its finite total cardinality is
contradicted by monotonicity and surjectivity of the first count.  Applying it
to increase versus equality and shifting starts by one yields the statement.

This formalizes the exact obstruction behind the source ambiguity: a positive
answer to a standard asymptotic-frequency reading already implies the famous
open consecutive-equal-totient problem.  It does not assume or assert that open
conclusion.

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