Every distance $\ge 0.3$ au is within $-25\%$ to $+50\%$ of a Titius–Bode position

Proved

TitiusBode.within_deviation_band

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

inequalitiestitius-bode

Let $a(n) = 0.4 + 0.3\cdot 2^n$ (astronomical units) be the Titius–Bode distance, for $n \in \{-\infty, 0, 1, 2, \dots\}$ with $2^{-\infty} = 0$ . For every real $d \ge 0.3$ there is an index $n$ such that the relative deviation of $d$ from $a(n)$ lies between $-25\%$ and $+50\%$ :

-\frac14 \;\le\; \frac{d - a(n)}{a(n)} \;\le\; \frac12 .

This is the observation recorded in footnote 1 of the data table of the source: since consecutive predicted distances roughly double, an arbitrary planet may be found within $-25\%$ to $+50\%$ of one of the predicted positions. The bound $d \ge 0.3 = \tfrac34\cdot 0.4$ is the range in which the claim holds; for $0 < d < 0.3$ no predicted position is close enough.

Formalization Note The source says "an arbitrary planet" without a range; the explicit hypothesis $d \ge 0.3$ is the exact range of validity.

Preamble

import Definitions.Def_TitiusBode_Defs
import Mathlib
open Filter Topology

Formal statement

namespace TitiusBode
theorem within_deviation_band (d : ℝ) (hd : 0.3 ≤ d) :
    ∃ n : WithBot ℕ, -0.25 ≤ deviation d (tbAU n) ∧ deviation d (tbAU n) ≤ 0.5 := 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 $d$ be any real number with $d \ge 0.3$ . The statement asserts that there exists $n \in \{\bot\} \cup \mathbb N$ (where $\bot$ plays the role of $-\infty$ ) such that, writing

A(n) = 0.4 + 0.3\,E(n), \qquad E(\bot) = 0,\; E(k) = 2^k \ (k \in \mathbb N),

both inequalities

-0.25 \le \frac{d - A(n)}{A(n)} \quad\text{and}\quad \frac{d - A(n)}{A(n)} \le 0.5

hold. Here the quotient is the deviation function, defined as real division with the convention $x/0 = 0$ ; since $A(n) \ge 0.4 > 0$ for every $n$ , this convention never applies. The only hypothesis is $d \ge 0.3$ ; there is no upper bound on $d$ . The decimals $0.3, 0.25, 0.5$ are exact rational numbers.

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

Every distance ≥0.3\ge 0.3≥0.3 au is within −25%-25\%−25% to +50%+50\%+50% of a Titius–Bode position

Every distance $\ge 0.3$ au is within $-25\%$ to $+50\%$ of a Titius–Bode position