Footnote 1 — consecutive distances less than double, ratio tending to $2$

Proved

TitiusBode.ratio_to_previous

by Lucas · Oct 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

limitstitius-bode

Let $a(n) = 0.4 + 0.3\cdot 2^n$ for $n \in \{-\infty, 0, 1, \dots\}$ and $a_n$ the same expression for $n \in \mathbb N$ . Then

$a(0) < 2\,a(-\infty)$ , i.e. $0.7 < 0.8$ ;
$a_{n+1} < 2a_n$ for every $n \in \mathbb N$ ;
$\displaystyle \lim_{n\to\infty} \frac{a_{n+1}}{a_n} = 2$ .

This is the first sentence of footnote 1 to the data table of the source: for large $k$ each Titius–Bode distance is approximately twice the preceding value, while for small $k$ the predicted distances do not fully double.

Preamble

import Definitions.Def_TitiusBode_Defs
import Mathlib
open Filter Topology

Formal statement

namespace TitiusBode
theorem ratio_to_previous :
    tbAU ((0 : ℕ) : WithBot ℕ) < 2 * tbAU ⊥ ∧
    (∀ n : ℕ, tbCanonical (n + 1) < 2 * tbCanonical n) ∧
    Tendsto (fun n : ℕ => tbCanonical (n + 1) / tbCanonical n) atTop (𝓝 2) := by sorry
end TitiusBode

Source

Wikipedia, "Titius–Bode law", revision oldid=1372822920, https://en.wikipedia.org/w/index.php?title=Titius%E2%80%93Bode_law&oldid=1372822920, section "Data", footnote 1 to the table

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic) — non-blind, same agent as the drafter

Non-blind read-back — not independent testimony. This read-back was written by the same agent that drafted the Lean statements, at the explicit request of the proposal owner. Its author knew the intended meaning and the source material, so it is not a blind audit and must not be mistaken for independent testimony; reviewers should compare the Lean code against the source themselves.

No hypotheses. With $A$ the AU form ( $A(\bot) = 0.4$ , $A(n) = 0.4 + 0.3\cdot 2^n$ ) and $a_n = 0.4 + 0.3\cdot 2^n$ for $n \in \mathbb N$ , the statement asserts the conjunction of:

$A(0) < 2\,A(\bot)$ (strict);
for every $n \in \mathbb N$ : $a_{n+1} < 2a_n$ (strict);
the real sequence $n \mapsto a_{n+1}/a_n$ converges to $2$ as $n \to \infty$ (convergence in the usual topology of $\mathbb R$ along $n \to \infty$ in $\mathbb N$ ).

Human review

Endorsed by Shuze Chen · Oct 10, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 10, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Footnote 1 — consecutive distances less than double, ratio tending to 222

Footnote 1 — consecutive distances less than double, ratio tending to $2$