Recursive form — $a_{n+1} = 2a_n - 0.4$ , and the index shift of $a_0 = 0.55$

Proved

TitiusBode.recursive_form

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

recurrencesequencestitius-bode

Let $a_n = 0.4 + 0.3\cdot 2^n$ ( $n \in \mathbb N$ ) be the canonical Titius–Bode form, and let $b$ be the recursive sequence printed in the source, $b_0 = 0.55$ and $b_{n+1} = 2b_n - 0.4$ . Then

the canonical form satisfies the recursion: $a_{n+1} = 2a_n - 0.4$ for all $n$ ;
the printed recursion reproduces the canonical form shifted by one index: $b_{n+1} = a_n$ for all $n$ ;
$b_0 \ne a_0$ (indeed $b_0 = 0.55$ while $a_0 = 0.7$ ).

The source states that the canonical form "also has a recursive form $a_{n+1} = 2a_n - 0.4$ , where $a_0 = 0.55$ ". Read literally with the same index, that claim is false; this milestone records the correct relationship.

Preamble

import Definitions.Def_TitiusBode_Defs
import Mathlib
open Filter Topology

Formal statement

namespace TitiusBode
theorem recursive_form :
    (∀ n : ℕ, tbCanonical (n + 1) = 2 * tbCanonical n - 0.4) ∧
    (∀ n : ℕ, tbRecursive (n + 1) = tbCanonical n) ∧
    tbRecursive 0 ≠ tbCanonical 0 := 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", last paragraph

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\cdot 2^n$ for $n \in \mathbb N$ and the real sequence $b_0 = 0.55$ , $b_{n+1} = 2b_n - 0.4$ , the statement asserts the conjunction of:

for every $n \in \mathbb N$ : $a_{n+1} = 2a_n - 0.4$ ;
for every $n \in \mathbb N$ : $b_{n+1} = a_n$ ;
$b_0 \ne a_0$ .

All decimals 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

Recursive form — an+1=2an−0.4a_{n+1} = 2a_n - 0.4an+1​=2an​−0.4, and the index shift of a0=0.55a_0 = 0.55a0​=0.55

Recursive form — $a_{n+1} = 2a_n - 0.4$ , and the index shift of $a_0 = 0.55$