---
id: F-004
title: Sub-triple-log decreasing runs obstruct the proposed asymptotic
tier: lean
polarity: negative
depends_on: [F-003]
supersedes: []
verifier: export PATH="$HOME/.elan/bin:$PATH"; diff -u verified_math/F-004_subtriplelog-obstruction/lean/Research/Structural.lean workspace/experiments/experiment_1_formalize_patterns/lean/Research/Structural.lean && (cd workspace/experiments/experiment_1_formalize_patterns/lean && lake build)
date: 2026-07-11
---

## Statement

With `F`, `G`, and `tripleLog(n)=log(log(log n))` as in F-001 and F-003, if

\[
\frac{G(n)}{\log\log\log n}\longrightarrow 0,
\]

then the same ratio for `F` tends to zero, and therefore there is no positive
constant `c` for which `F(n)=(c+o(1))log log log n`.

Formal conclusions:

```lean
theorem F_ratio_tendsto_zero
    (hG : Tendsto (fun n : ℕ => (G n : ℝ) / tripleLog n) atTop (𝓝 0)) :
    Tendsto (fun n : ℕ => (F n : ℝ) / tripleLog n) atTop (𝓝 0)

theorem not_asymptotic_of_G_ratio_zero (hG : ...) : ¬ AsymptoticQuestion
```

This is a **conditional reduction**, not a formal proof of the deep analytic
hypothesis `hG`.

## Proof / verification

Three compositions of `Real.tendsto_log_atTop` show that the denominator tends
to infinity and is eventually positive.  F-003 gives `0≤F(n)≤G(n)`; division
by the eventually positive denominator and the squeeze theorem yield the zero
limit.  Uniqueness of limits contradicts the positive constant required by
`AsymptoticQuestion`.

Lean's kernel accepts the theorem with no `sorry`, `admit`, or axioms.  Frozen
sources and project metadata are in `lean/`.
