---
id: F-028
title: Canonical eventual-frequency reading implies Erdős #1003
tier: lean
polarity: positive
depends_on: [F-027]
supersedes: []
verifier: export PATH="$HOME/.elan/bin:$PATH"; diff -u verified_math/F-028_canonical-third-question-obstruction/lean/Research/WeakCanonical.lean workspace/experiments/experiment_1_formalize_patterns/lean/Research/WeakCanonical.lean && (cd workspace/experiments/experiment_1_formalize_patterns/lean && lake build)
date: 2026-07-11
---

## Statement

Formalize the literal eventual finite-cutoff reading at length two:
`EventuallyNaturalIsMostFrequentK2` says that for all sufficiently large
cutoffs, the weak order of `(φ(1),φ(2))=(1,1)` has at least as many starts as
every weak rank pattern.  Then

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

Thus even this canonical positive reading implies the open consecutive-equal-
totient problem.

## Proof / verification

The proof first identifies the exact finite weak-pattern count at cutoff `N+1`
with `Nat.count` of matching starts below `N`.  Explicit `Fin 2` comparison
lemmas show that the identity ranks mean strict increase while the natural
reference means equality.  Eventual maximality therefore implies F-027's
eventual equality-over-increase dominance, and F-027 yields infinitely many
solutions of `φ(n)=φ(n+1)`.

This is a statement-fidelity result, not an assumption of #1003.  It rigorously
shows why the source's unspecified third question cannot simply be declared an
asymptotic theorem without selecting a meaning that reaches a separate open
problem.  `#print axioms` reports only `propext`, `Classical.choice`, and
`Quot.sound`.

Artifact: `lean/Research/WeakCanonical.lean`; full `lake build` succeeds with no
`sorry`, `admit`, native evaluator axiom, or project-declared axiom.
