Data table — the predicted Titius–Bode distances

Proved

TitiusBode.data_table_predictions

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

computationtitius-bode

The Titius–Bode distances $a(n) = 0.4 + 0.3\cdot 2^n$ (au) are, for $n = -\infty, 0, 1, \dots, 8$ :

0.4,\; 0.7,\; 1.0,\; 1.6,\; 2.8,\; 5.2,\; 10.0,\; 19.6,\; 38.8,\; 77.2 .

The first nine values form the "T–B rule distance" column of the data table of the source (Mercury, Venus, Earth, Mars, Ceres, Jupiter, Saturn, Uranus, Pluto); the values $10.0, 19.6, 38.8, 77.2$ for $n = 5, \dots, 8$ are the "about $10, 20, 39$ and $77$ au" quoted for Saturn, Uranus, Neptune and Pluto in the section "Original formulation".

Preamble

import Definitions.Def_TitiusBode_Defs
import Mathlib
open Filter Topology

Formal statement

namespace TitiusBode
theorem data_table_predictions :
    tbAU ⊥ = 0.4 ∧ tbAU ((0 : ℕ) : WithBot ℕ) = 0.7 ∧ tbAU ((1 : ℕ) : WithBot ℕ) = 1.0 ∧
    tbAU ((2 : ℕ) : WithBot ℕ) = 1.6 ∧ tbAU ((3 : ℕ) : WithBot ℕ) = 2.8 ∧
    tbAU ((4 : ℕ) : WithBot ℕ) = 5.2 ∧ tbAU ((5 : ℕ) : WithBot ℕ) = 10.0 ∧
    tbAU ((6 : ℕ) : WithBot ℕ) = 19.6 ∧ tbAU ((7 : ℕ) : WithBot ℕ) = 38.8 ∧
    tbAU ((8 : ℕ) : WithBot ℕ) = 77.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" (table, column "T–B rule distance (AU)") and 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.

No hypotheses. With $A(n) = 0.4 + 0.3\,E(n)$ , $E(\bot) = 0$ , $E(k) = 2^k$ , the statement asserts the ten exact equalities of real numbers

A(\bot) = 0.4,\ A(0) = 0.7,\ A(1) = 1.0,\ A(2) = 1.6,\ A(3) = 2.8,\ A(4) = 5.2,

A(5) = 10.0,\ A(6) = 19.6,\ A(7) = 38.8,\ A(8) = 77.2,

where $0, 1, \dots, 8$ are natural numbers viewed in $\{\bot\}\cup\mathbb N$ and all decimals are exact rationals.

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