Footnote 1 — any at-most-doubling unbounded sequence covers with a $-25\%/+50\%$ band

Proved

TitiusBode.doubling_covering

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

inequalitiessequencestitius-bode

Let $(p_k)_{k\ge 0}$ be a sequence of real numbers that at most doubles at each step and is unbounded above:

$p_{k+1} \le 2p_k$ for all $k$ ;
for every $M \in \mathbb R$ there is $k$ with $p_k \ge M$ .

Then for every real $d \ge \tfrac34 p_0$ there is $k$ with

-\frac14 \;\le\; \frac{d - p_k}{p_k} \;\le\; \frac12 .

This is the general principle behind footnote 1 to the data table of the source ("each Titius–Bode rule distance is approximately twice the preceding value. Hence, an arbitrary planet may be found within $-25\%$ to $+50\%$ of one of the predicted positions"); it applies to any Titius–Bode-type rule whose consecutive ratios do not exceed $2$ .

Preamble

import Definitions.Def_TitiusBode_Defs
import Mathlib
open Filter Topology

Formal statement

namespace TitiusBode
theorem doubling_covering (p : ℕ → ℝ) (hstep : ∀ k, p (k + 1) ≤ 2 * p k)
    (hunbdd : ∀ M : ℝ, ∃ k, M ≤ p k) (d : ℝ) (hd : 3 / 4 * p 0 ≤ d) :
    ∃ k, -1 / 4 ≤ deviation d (p k) ∧ deviation d (p k) ≤ 1 / 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.

Let $p : \mathbb N \to \mathbb R$ be any real sequence and $d$ any real number. Hypotheses:

for every $k \in \mathbb N$ : $p_{k+1} \le 2p_k$ ;
for every real $M$ there exists $k \in \mathbb N$ with $M \le p_k$ ;
$\tfrac34\, p_0 \le d$ .

Conclusion: there exists $k \in \mathbb N$ with

-\tfrac14 \le \operatorname{dev}(d, p_k) \quad\text{and}\quad \operatorname{dev}(d, p_k) \le \tfrac12,

where $\operatorname{dev}(d, p) = (d - p)/p$ with the convention $x/0 = 0$ . No positivity of $p$ is assumed explicitly (no hypothesis says $p_0 > 0$ ); no monotonicity is assumed.

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 — any at-most-doubling unbounded sequence covers with a −25%/+50%-25\%/+50\%−25%/+50% band

Footnote 1 — any at-most-doubling unbounded sequence covers with a $-25\%/+50\%$ band