Dermott's law — geometric periods and Titius–Bode-type geometric distances

Proved

TitiusBode.dermott_geometric_spacing

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

dermott-lawpower-lawtitius-bode

Let $T(n) = T(0)\,C^n$ be Dermott's law with $T(0) > 0$ and $C > 0$ , and let $K$ be any real constant. Then for every $n$ :

consecutive periods have constant ratio: $T(n+1)/T(n) = C$ ;
the Keplerian semi-major axes $a(n) = K\,T(n)^{2/3}$ form a geometric progression with ratio $C^{2/3}$ :

a(n+1) = C^{2/3}\, a(n).

The Dermott article presents its law as a power law of the same kind as the Titius–Bode law, and the Titius–Bode article (section "Natural satellite systems and exoplanetary systems") calls it a "slight new phrasing" of that law; this milestone records the precise relationship between the period law and a geometric distance law.

Formalization Note The statement holds for all $n \ge 0$ ; the source indexes satellites by $n = 1, 2, 3, \dots$ .

Preamble

import Definitions.Def_TitiusBode_Defs
import Mathlib
open Filter Topology

Formal statement

namespace TitiusBode
theorem dermott_geometric_spacing (T₀ C K : ℝ) (hT₀ : 0 < T₀) (hC : 0 < C) (n : ℕ) :
    dermottPeriod T₀ C (n + 1) / dermottPeriod T₀ C n = C ∧
    K * dermottPeriod T₀ C (n + 1) ^ ((2 : ℝ) / 3) =
      C ^ ((2 : ℝ) / 3) * (K * dermottPeriod T₀ C n ^ ((2 : ℝ) / 3)) := by sorry
end TitiusBode

Source

Wikipedia, "Dermott's law", revision oldid=1315813288, https://en.wikipedia.org/w/index.php?title=Dermott%27s_law&oldid=1315813288; Wikipedia, "Titius–Bode law", revision oldid=1372822920, https://en.wikipedia.org/w/index.php?title=Titius%E2%80%93Bode_law&oldid=1372822920, section "Natural satellite systems and exoplanetary systems" and footnote 1 (semi-major axis proportional to the 2/3 power of the period)

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 $T_0, C, K$ be real numbers with $T_0 > 0$ and $C > 0$ ( $K$ unrestricted), and let $n \in \mathbb N$ (including $n = 0$ ). With $T(m) = T_0\, C^m$ , the statement asserts both

\frac{T(n+1)}{T(n)} = C \quad\text{and}\quad K\cdot T(n+1)^{2/3} = C^{2/3}\cdot\bigl(K\cdot T(n)^{2/3}\bigr),

where the quotient is real division and $t^{2/3}$ is the real power function.

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