---
id: F-023
title: Eventual successor stability of the triple logarithm
tier: lean
polarity: positive
depends_on: [F-003]
supersedes: []
verifier: export PATH="$HOME/.elan/bin:$PATH"; diff -u verified_math/F-023_triplelog-successor-comparison/lean/Research/TripleLogShift.lean workspace/experiments/experiment_2_elementary_upper_bound/lean/Research/TripleLogShift.lean && (cd workspace/experiments/experiment_2_elementary_upper_bound/lean && lake build)
date: 2026-07-11
---

## Statement

For all sufficiently large natural `X`,

\[
 \log\log\log(X+1)\le 2\log\log\log X.
\]

Formal theorem: `eventually_tripleLog_succ_le_two`.

## Proof / verification

Eventually `X≥2` and `log log X≥2`.  Then `X+1≤X²`; applying logarithmic
monotonicity successively gives bounds by `2 log X`, then `2 log log X`, then
`2 log log log X`.  Lean verifies every positivity side condition.

Artifact: `lean/Research/TripleLogShift.lean`; accepted without `sorry`,
`admit`, or axioms.
