theorem
proved
r_orbit_zero
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Astrophysics.PlanetaryFormationFromJCost on GitHub at line 87.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
84 unfold r_orbit
85 exact mul_pos h (pow_pos phi_pos k)
86
87theorem r_orbit_zero (r0 : ℝ) : r_orbit r0 0 = r0 := by
88 unfold r_orbit
89 simp
90
91theorem r_orbit_succ (r0 : ℝ) (k : ℕ) :
92 r_orbit r0 (k + 1) = r_orbit r0 k * phi := by
93 unfold r_orbit
94 rw [pow_succ]
95 ring
96
97/-- Adjacent ratio is exactly φ. -/
98theorem r_orbit_adjacent_ratio (r0 : ℝ) (h : 0 < r0) (k : ℕ) :
99 r_orbit r0 (k + 1) / r_orbit r0 k = phi := by
100 have hk : r_orbit r0 k > 0 := r_orbit_pos r0 h k
101 rw [r_orbit_succ]
102 field_simp
103
104/-- Strict monotonicity: outer rung is strictly farther than inner rung. -/
105theorem r_orbit_strict_mono (r0 : ℝ) (h : 0 < r0) (k : ℕ) :
106 r_orbit r0 k < r_orbit r0 (k + 1) := by
107 rw [r_orbit_succ]
108 have hk : 0 < r_orbit r0 k := r_orbit_pos r0 h k
109 have h1 : 1 < phi := one_lt_phi
110 nlinarith [r_orbit_pos r0 h k, one_lt_phi]
111
112/-- Closed form. -/
113theorem r_orbit_closed (r0 : ℝ) (k : ℕ) :
114 r_orbit r0 k = r0 * phi ^ k := rfl
115
116/-! ## §2. Numerical bands for the canonical Titius-Bode ratio -/
117