pith. machine review for the scientific record. sign in
theorem proved tactic proof

r_orbit_gap_skip_band

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 126theorem r_orbit_gap_skip_band (r0 : ℝ) (h : 0 < r0) (k : ℕ) :
 127    (2.5 : ℝ) < r_orbit r0 (k + 2) / r_orbit r0 k ∧
 128    r_orbit r0 (k + 2) / r_orbit r0 k < 2.7 := by

proof body

Tactic-mode proof.

 129  have hk : 0 < r_orbit r0 k := r_orbit_pos r0 h k
 130  have hr0 : r0 ≠ 0 := ne_of_gt h
 131  have hphi_k : phi ^ k ≠ 0 := pow_ne_zero _ phi_ne_zero
 132  have hratio :
 133      r_orbit r0 (k + 2) / r_orbit r0 k = phi ^ 2 := by
 134    unfold r_orbit
 135    rw [show (k + 2) = k + 2 from rfl, pow_add]
 136    field_simp
 137  rw [hratio]
 138  exact phi_squared_bounds
 139
 140/-! ## §3. The asteroid-belt / gap-skip identity -/
 141
 142/-- Two-rung gap (e.g. Mars → Jupiter, skipping the asteroid-belt
 143rung) has cumulative ratio `φ²`. -/

used by (3)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (21)

Lean names referenced from this declaration's body.