Footnote 1 — $2{:}3$ resonance: distances differ by $-23.69\%$ and $+31.04\%$

Proved

TitiusBode.resonance_two_three

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

numerical-boundsorbital-resonancetitius-bode

Let $K > 0$ and let $T_1, T_2$ be orbital periods with $T_1 > 0$ and $T_1 / T_2 = 2/3$ (a $2{:}3$ orbital resonance). Suppose the semi-major axes are given by Kepler's third law, $a_i = K\,T_i^{2/3}$ . Then, rounded to two decimals, the relative deviations are

100\cdot\frac{a_1 - a_2}{a_2} \approx -23.69, \qquad 100\cdot\frac{a_2 - a_1}{a_1} \approx +31.04,

in the precise sense that each differs from the printed value by less than $0.005$ .

This is the last sentence of footnote 1 to the data table of the source: planets in a $2{:}3$ orbital resonance vary in distance by $(2/3)^{2/3}$ , i.e. $-23.69\%$ and $+31.04\%$ relative to one another.

Formalization Note Kepler's law appears only as the form $a_i = K T_i^{2/3}$ of the two semi-major axes; $T_i^{2/3}$ is the real power.

Preamble

import Definitions.Def_TitiusBode_Defs
import Mathlib
open Filter Topology

Formal statement

namespace TitiusBode
theorem resonance_two_three (K T₁ T₂ : ℝ) (hK : 0 < K) (hT₁ : 0 < T₁)
    (hres : T₁ / T₂ = 2 / 3) :
    |100 * deviation (K * T₁ ^ ((2 : ℝ) / 3)) (K * T₂ ^ ((2 : ℝ) / 3)) - (-23.69)| < 0.005 ∧
    |100 * deviation (K * T₂ ^ ((2 : ℝ) / 3)) (K * T₁ ^ ((2 : ℝ) / 3)) - 31.04| < 0.005 := 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", footnote 1 to the table (last two sentences)

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 $K, T_1, T_2$ be real numbers with $K > 0$ , $T_1 > 0$ and $T_1 / T_2 = 2/3$ (real division with $x/0 = 0$ ; since $2/3 \ne 0$ this forces $T_2 \ne 0$ , hence $T_2 = \tfrac32 T_1 > 0$ ). Put $a_1 = K\,T_1^{2/3}$ and $a_2 = K\,T_2^{2/3}$ , where $t^{2/3}$ is the real power function. The statement asserts both

\left|\,100\cdot\frac{a_1 - a_2}{a_2} - (-23.69)\right| < 0.005 \quad\text{and}\quad \left|\,100\cdot\frac{a_2 - a_1}{a_1} - 31.04\right| < 0.005,

where each quotient is the deviation function $(d-p)/p$ (with $x/0 = 0$ ). 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

Footnote 1 — 2:32{:}32:3 resonance: distances differ by −23.69%-23.69\%−23.69% and +31.04%+31.04\%+31.04%

Footnote 1 — $2{:}3$ resonance: distances differ by $-23.69\%$ and $+31.04\%$