Original formulation — the four representations of the Titius–Bode rule agree

Proved

TitiusBode.representations_agree

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

sequencestitius-bode

Let $x = 0, 3, 6, 12, \dots$ be the sequence $x_0 = 0$ , $x_1 = 3$ , $x_{i+2} = 2x_{i+1}$ . Then:

the original values $4 + x_i$ (Earth $= 10$ ) equal $4 + 3\cdot 2^{n}$ with $n = -\infty$ for $i = 0$ and $n = i - 1$ for $i \ge 1$ :

4 + x_0 = 4 + 3\cdot 2^{-\infty}, \qquad 4 + x_{n+1} = 4 + 3\cdot 2^{n}\quad (n \in \mathbb N);

dividing by $10$ converts to astronomical units: $0.4 + 0.3\cdot 2^n = (4 + 3\cdot 2^n)/10$ for all $n \in \{-\infty, 0, 1, \dots\}$ ;
for $n \in \mathbb N$ the au form coincides with the canonical form $a_n = 0.4 + 0.3\cdot 2^n$ .

This records that the representations given in the section "Original formulation" of the source describe the same predicted distances.

Preamble

import Definitions.Def_TitiusBode_Defs
import Mathlib
open Filter Topology

Formal statement

namespace TitiusBode
theorem representations_agree :
    ((tbOriginal 0 : ℝ) = tbTenths ⊥ ∧
      ∀ n : ℕ, (tbOriginal (n + 1) : ℝ) = tbTenths (n : WithBot ℕ)) ∧
    (∀ n : WithBot ℕ, tbAU n = tbTenths n / 10) ∧
    (∀ n : ℕ, tbAU (n : WithBot ℕ) = tbCanonical n) := 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 "Original formulation"

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.

The statement is a conjunction of three parts, with no hypotheses.

(a) $4 + x_0 = 4 + 3E(\bot)$ as real numbers, where $x_0 = 0$ and $E(\bot) = 0$ ; (b) for every $n \in \mathbb N$ , $4 + x_{n+1} = 4 + 3\cdot 2^n$ as real numbers. Here $x$ is the natural-number sequence $x_0 = 0$ , $x_1 = 3$ , $x_{i+2} = 2x_{i+1}$ , and the left sides are the natural numbers $4 + x_i$ cast to $\mathbb R$ .
For every $n \in \{\bot\}\cup\mathbb N$ : $0.4 + 0.3\,E(n) = (4 + 3E(n))/10$ .
For every $n \in \mathbb N$ : $0.4 + 0.3\,E(n) = 0.4 + 0.3\cdot 2^n$ , where on the left $n$ is viewed as an element of $\{\bot\}\cup\mathbb N$ .

$E$ is the extended power of two: $E(\bot) = 0$ , $E(n) = 2^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