Titius–Bode and Dermott laws: basic definitions

Definition

TitiusBode_Defs

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

mathematical-physicssequencestitius-bode

Basic objects of the Titius–Bode and Dermott laws.

The extended power of two $2^n$ for $n \in \{-\infty, 0, 1, 2, \dots\}$ , with $2^{-\infty} = 0$ .
The sequence $x_0 = 0$ , $x_1 = 3$ , $x_{i+2} = 2x_{i+1}$ , i.e. $x = 0, 3, 6, 12, 24, \dots$ , and the original formulation $a = 4 + x_i$ (Earth $= 10$ ).
The form $a(n) = 4 + 3\cdot 2^n$ (Earth $= 10$ ) and the form in astronomical units $a(n) = 0.4 + 0.3 \cdot 2^n$ , both for $n \in \{-\infty, 0, 1, 2, \dots\}$ .
The canonical form $a_n = 0.4 + 0.3\cdot 2^n$ for $n \in \mathbb N$ .
The recursive form as printed in the source: $a_0 = 0.55$ , $a_{n+1} = 2a_n - 0.4$ .
The relative deviation $(d - p)/p$ of an observed value $d$ from a prediction $p$ .
Dermott's law $T(n) = T(0)\,C^n$ .

These are the shared definitions for every statement of the mission.

Formalization Note The exponent $-\infty$ is the bottom element of the natural numbers with a bottom adjoined. The deviation is the plain real quotient (Lean returns $0$ when $p = 0$ ); statements only use it at positive $p$ . Dermott's period is defined for every $n \in \mathbb N$ ; the source uses $n \ge 1$ .

Definition code

import Mathlib

namespace TitiusBode

/-- The extended power of two used by the Titius–Bode law: `2 ^ n` for a natural
number `n`, and `2 ^ (-∞) = 0` for the formal exponent `n = -∞` (encoded as `⊥`). -/
noncomputable def twoPowExt : WithBot ℕ → ℝ
  | ⊥ => 0
  | (n : ℕ) => 2 ^ n

/-- The sequence `x = 0, 3, 6, 12, 24, 48, 96, 192, 384, 768, …` of the original
Titius–Bode formulation: `x₀ = 0`, `x₁ = 3`, and from then on each value is twice the
previous one. -/
def tbX : ℕ → ℕ
  | 0 => 0
  | 1 => 3
  | (i + 2) => 2 * tbX (i + 1)

/-- The original Titius–Bode formulation `a = 4 + x`, in units in which the Earth's
semi-major axis equals `10`; `i = 0, 1, 2, …` indexes the terms of `x`. -/
def tbOriginal (i : ℕ) : ℕ := 4 + tbX i

/-- The second representation `a = 4 + 3 × 2 ^ n`, `n = -∞, 0, 1, 2, …`, in units in
which the Earth's semi-major axis equals `10`. -/
noncomputable def tbTenths (n : WithBot ℕ) : ℝ := 4 + 3 * twoPowExt n

/-- The Titius–Bode distance in astronomical units, `a = 0.4 + 0.3 × 2 ^ n`,
`n = -∞, 0, 1, 2, …`. These are the predicted positions of the law. -/
noncomputable def tbAU (n : WithBot ℕ) : ℝ := 0.4 + 0.3 * twoPowExt n

/-- The "classical" (canonical) form `aₙ = 0.4 + 0.3 × 2 ^ n`, `n = 0, 1, 2, …`. -/
noncomputable def tbCanonical (n : ℕ) : ℝ := 0.4 + 0.3 * 2 ^ n

/-- The "recursive" form as printed in the source: `a₀ = 0.55` and
`aₙ₊₁ = 2 × aₙ - 0.4`. -/
noncomputable def tbRecursive : ℕ → ℝ
  | 0 => 0.55
  | (n + 1) => 2 * tbRecursive n - 0.4

/-- Relative deviation of an observed value from a predicted value,
`(observed - predicted) / predicted` (multiply by `100` for a percentage). -/
noncomputable def deviation (observed predicted : ℝ) : ℝ :=
  (observed - predicted) / predicted

/-- Dermott's law: the orbital period of the `n`-th satellite is `T(n) = T(0) · C ^ n`
(the source uses `n = 1, 2, 3, …`). -/
noncomputable def dermottPeriod (T₀ C : ℝ) (n : ℕ) : ℝ := T₀ * C ^ n

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, sections "Original formulation" and "Data"; Wikipedia, "Dermott's law", revision oldid=1315813288, https://en.wikipedia.org/w/index.php?title=Dermott%27s_law&oldid=1315813288

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 file declares, inside the namespace TitiusBode, the following objects (all real-valued unless stated).

Extended power of two $E : \{\bot\} \cup \mathbb N \to \mathbb R$ with $E(\bot) = 0$ and $E(n) = 2^n$ for $n \in \mathbb N$ .
Sequence $x : \mathbb N \to \mathbb N$ with $x_0 = 0$ , $x_1 = 3$ , $x_{i+2} = 2\,x_{i+1}$ . Hence $x_i = 3\cdot 2^{i-1}$ for $i \ge 1$ .
Original value $O(i) = 4 + x_i \in \mathbb N$ .
Tenths form $A_{10}(n) = 4 + 3E(n)$ for $n \in \{\bot\}\cup\mathbb N$ .
AU form $A(n) = 0.4 + 0.3\,E(n)$ for $n \in \{\bot\}\cup\mathbb N$ ; so $A(\bot) = 0.4$ and $A(n) = 0.4 + 0.3\cdot 2^n$ .
Canonical form $a_n = 0.4 + 0.3 \cdot 2^n$ for $n \in \mathbb N$ .
Recursive sequence $b_0 = 0.55$ , $b_{n+1} = 2b_n - 0.4$ .
Deviation $\operatorname{dev}(d, p) = (d - p)/p$ , with the convention that division by $0$ gives $0$ , so $\operatorname{dev}(d, 0) = 0$ for every $d$ .
Dermott period $T(T_0, C, n) = T_0\, C^n$ for real $T_0, C$ and every $n \in \mathbb N$ (including $n = 0$ ), with no sign restrictions.

No hypotheses or theorems are contained in the file; it is sorry-free.

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