---
id: F-025
title: The proposed positive triple-log asymptotic is false
tier: lean
polarity: negative
depends_on: [F-004, F-022, F-023, F-024]
supersedes: []
verifier: export PATH="$HOME/.elan/bin:$PATH"; diff -u verified_math/F-025_no-positive-triplelog-asymptotic/lean/Research/DecreasingRunAsymptotic.lean workspace/experiments/experiment_2_elementary_upper_bound/lean/Research/DecreasingRunAsymptotic.lean && (cd workspace/experiments/experiment_2_elementary_upper_bound/lean && lake build)
date: 2026-07-11
---

## Statement

Let `G(X)` be the maximum length of a strictly decreasing consecutive totient
block ending by `X`.  Then

\[
 \frac{G(X)}{\log\log\log X}\longrightarrow 0.
\]

Consequently `F(X)/log log log X→0`, so there is no positive constant `c` for
which `F(X)=(c+o(1))log log log X`.

Formal theorems:

```lean
theorem G_ratio_tendsto_zero :
  Tendsto (fun X : ℕ ↦ (G X : ℝ) / tripleLog X) atTop (𝓝 0)

theorem not_AsymptoticQuestion : ¬ AsymptoticQuestion
```

## Proof / verification

Fix an arbitrary target coefficient `b>0`.  F-024, at a sufficiently large
rate `R`, extracts from every long decreasing block a tail of length at least
`n-B` whose loss is at least `Rℓ`.  F-022 bounds the same loss by
`Cℓ+A log log log(X+1)`, and F-023 replaces the final scale by at most twice
`log log log X`.  Choosing `R=C+8A/b` and absorbing the fixed `B` gives
`G(X)<b log log log X` eventually.  Nonnegativity gives convergence to zero.
F-004 then transfers this to `F` and negates every positive limiting constant.

The artifact also proves that `G(X)` is genuinely witnessed (including the
zero-length base case).  Lean verifies all quantifiers, finite cutoffs,
positivity conditions, and limit arguments.  Artifact:
`lean/Research/DecreasingRunAsymptotic.lean`; the full project builds with no
`sorry`, `admit`, or axioms.
