 174
 175/-! ## §5. Master certificate -/
 176
 177structure PlanetaryFormationCert where
 178  r_orbit_pos : ∀ r0 : ℝ, 0 < r0 → ∀ k : ℕ, 0 < r_orbit r0 k
 179  r_orbit_zero : ∀ r0 : ℝ, r_orbit r0 0 = r0
 180  r_orbit_adjacent_ratio :
 181    ∀ r0 : ℝ, 0 < r0 → ∀ k : ℕ,
 182      r_orbit r0 (k + 1) / r_orbit r0 k = phi
 183  r_orbit_strict_mono :
 184    ∀ r0 : ℝ, 0 < r0 → ∀ k : ℕ,
 185      r_orbit r0 k < r_orbit r0 (k + 1)
 186  r_orbit_closed_form :
 187    ∀ r0 : ℝ, ∀ k : ℕ, r_orbit r0 k = r0 * phi ^ k
 188  r_orbit_adjacent_band :
 189    ∀ r0 : ℝ, 0 < r0 → ∀ k : ℕ,
 190      1.61 < r_orbit r0 (k + 1) / r_orbit r0 k ∧
 191      r_orbit r0 (k + 1) / r_orbit r0 k < 1.62
 192  r_orbit_gap_skip_band :
 193    ∀ r0 : ℝ, 0 < r0 → ∀ k : ℕ,
 194      (2.5 : ℝ) < r_orbit r0 (k + 2) / r_orbit r0 k ∧
 195      r_orbit r0 (k + 2) / r_orbit r0 k < 2.7
 196  ladder_agrees_at_half_rung :
 197    ∀ r0 : ℝ, 0 < r0 → ∀ k : ℕ,
 198      AgreesAtHalfRung r0 (r_orbit r0 k)
 199
 200def planetaryFormationCert : PlanetaryFormationCert where
 201  r_orbit_pos := r_orbit_pos
 202  r_orbit_zero := r_orbit_zero
 203  r_orbit_adjacent_ratio := r_orbit_adjacent_ratio
 204  r_orbit_strict_mono := r_orbit_strict_mono
 205  r_orbit_closed_form := r_orbit_closed
 206  r_orbit_adjacent_band := r_orbit_adjacent_ratio_band
 207  r_orbit_gap_skip_band := r_orbit_gap_skip_band

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.